Documentation

HexNumberFieldMathlib.Embedding

source
noncomputable def Hex.AlgebraicNumber.toComplexHom :
AlgebraicNumber →+* ℂ

The interpretation as a field homomorphism.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    instance Hex.AlgebraicNumber.instCharZero_hexNumberFieldMathlib :
    CharZero AlgebraicNumber
    source
    noncomputable def Hex.AlgebraicNumber.toComplexAlgHom :
    AlgebraicNumber →ₐ[ℚ] ℂ

    The complex embedding respects the canonical rational algebra structure.

    Equations
    Instances For
      source
      @[simp]
      theorem Hex.AlgebraicNumber.natCast_toComplex (n : ℕ) :
      (↑n).toComplex = ↑n
      source
      @[simp]
      theorem Hex.AlgebraicNumber.intCast_toComplex (n : ℤ) :
      (↑n).toComplex = ↑n
      source
      @[simp]
      theorem Hex.AlgebraicNumber.ratCast_toComplex (q : ℚ) :
      (↑q).toComplex = ↑q
      source
      @[simp]
      theorem Hex.AlgebraicNumber.ofNat_toComplex (n : ℕ) [n.AtLeastTwo] :
      (OfNat.ofNat n).toComplex = OfNat.ofNat n