Documentation

HexNumberFieldMathlib.Basic

source
theorem Hex.ZPoly.CheckedIrreducible.irreducibleRat (p : ZPoly) [p.CheckedIrreducible] :
_root_.Irreducible (HexPolyZMathlib.toPolyℚ p)

A computationally checked irreducible integer polynomial remains irreducible after extension of coefficients to the rationals.

source
theorem Hex.ZPoly.CheckedIrreducible.separable (p : ZPoly) [p.CheckedIrreducible] :
(HexPolyZMathlib.toPolyℚ p).Separable

A computationally checked irreducible integer polynomial is separable over the rationals. The factorization correspondence supplies irreducibility; this is the semantic bridge used by quotient-root interpretation.

source
noncomputable def Hex.AlgebraicRoot.toComplex (a : AlgebraicRoot) :
ℂ

The complex value selected by a factorization-lazy algebraic root.

Equations
Instances For
    source
    theorem Hex.AlgebraicRoot.toComplex_isRoot (a : AlgebraicRoot) :
    Polynomial.eval a.toComplex (HexRootsMathlib.toPolyℂ a.p) = 0

    The selected value zeros the enclosing integer polynomial.

    source
    noncomputable def Hex.AlgebraicNumber.toComplex (a : AlgebraicNumber) :
    ℂ

    The complex value selected by a canonical algebraic number.

    Equations
    Instances For
      source
      theorem Hex.AlgebraicNumber.p_eq_minpoly (a : AlgebraicNumber) :
      (↑(DensePoly.leadingCoeff a.p))⁻¹ • HexPolyZMathlib.toPolyℚ a.p = minpoly ℚ a.toComplex

      A canonical algebraic number stores its primitive positive associate of the rational minimal polynomial.

      source
      noncomputable def Hex.PolyQuot.toComplex {p : ZPoly} {x : SimpleRoot p} (a : PolyQuot p x) (rep : RefinedIsolation p) (_h : SimpleRoot.mk rep = x) :
      ℂ

      Evaluate canonical fixed-field coordinates at their selected complex root. The representative and quotient equality are explicit inputs so this semantic map does not depend on an irreducibility proof.

      Equations
      Instances For
        source
        theorem Hex.PolyQuot.eval_reduceCoeffs {p : ZPoly} (f : DensePoly ℚ) (rep : RefinedIsolation p) :
        Polynomial.eval₂ (algebraMap ℚ ℂ) rep.root (HexPolyMathlib.toPolynomial (reduceCoeffs p f)) = Polynomial.eval₂ (algebraMap ℚ ℂ) rep.root (HexPolyMathlib.toPolynomial f)

        Reduction modulo the defining polynomial preserves evaluation at the selected root.

        source
        theorem Hex.PolyQuot.map_add {p : ZPoly} {x : SimpleRoot p} (a b : PolyQuot p x) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) :
        (a + b).toComplex rep h = a.toComplex rep h + b.toComplex rep h

        Fixed-presentation addition agrees with complex addition.

        source
        theorem Hex.PolyQuot.map_mul {p : ZPoly} {x : SimpleRoot p} (a b : PolyQuot p x) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) :
        (a * b).toComplex rep h = a.toComplex rep h * b.toComplex rep h

        Fixed-presentation multiplication agrees with complex multiplication.

        source
        theorem Hex.AlgebraicNumber.toComplex_injective :
        Function.Injective toComplex

        Canonical algebraic numbers are determined by their represented complex value.

        source
        @[simp]
        theorem Hex.AlgebraicNumber.zero_toComplex :
        toComplex 0 = 0

        Canonical zero denotes complex zero.

        source
        theorem Hex.AlgebraicNumber.ofNormalized?_toComplex (p : ZPoly) (prim : p.Primitive) (pos_lc : 0 < DensePoly.leadingCoeff p) (pos_degree : 0 < DensePoly.natDegree p) (checked : p.CheckedIrreducible) (squarefree : HasOnlySimpleRoots p) (rep : RefinedIsolation p) {a : AlgebraicNumber} (h : ofNormalized? p prim pos_lc pos_degree checked squarefree rep = some a) :
        a.toComplex = rep.root

        Successful canonicalization preserves the complex root selected by the supplied refined isolation, including the explicit canonical-zero path.

        source
        theorem Hex.AlgebraicNumber.beq_iff (a b : AlgebraicNumber) :
        (a == b) = true ↔ a.toComplex = b.toComplex

        Canonical Boolean equality is equality of represented complex values.

        source
        instance Hex.instLawfulBEqAlgebraicNumber_hexNumberFieldMathlib :
        LawfulBEq AlgebraicNumber

        Canonical Boolean equality agrees with Lean equality.

        source
        @[instance_reducible]
        instance Hex.instDecidableEqAlgebraicNumber_hexNumberFieldMathlib :
        DecidableEq AlgebraicNumber

        Propositional equality is decided by canonical Boolean equality.

        Equations
        source
        theorem Hex.AlgebraicRoot.isZero_iff (a : AlgebraicRoot) :
        a.isZero = true ↔ a.toComplex = 0

        The executable zero predicate recognizes exactly the complex value zero.

        source
        theorem Hex.AlgebraicNumber.isZero_iff (a : AlgebraicNumber) :
        a.isZero = true ↔ a.toComplex = 0

        The canonical algebraic-number zero test recognizes exactly complex zero.