Documentation

HexResultant.FractionPoly

source
theorem Hex.Fraction.NonzeroOne.of_poly_ne_zero {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] (p : DensePoly R) (hp : p ≠ 0) :
NonzeroOne R

A nonzero dense polynomial supplies a nonzero coefficient and hence a nontrivial coefficient ring.

source
noncomputable def Hex.DensePoly.Fraction.map {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] [Fraction.NonzeroOne R] (p : DensePoly R) :
DensePoly (Fraction R)

Embed every coefficient of a dense polynomial into the fraction field.

Equations
Instances For
    source
    @[simp]
    theorem Hex.DensePoly.Fraction.coeff_map {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] [Fraction.NonzeroOne R] (p : DensePoly R) (n : Nat) :
    (map p).coeff n = Fraction.ofCoeff (p.coeff n)

    Coefficients commute with the fraction-field embedding.

    source
    @[simp]
    theorem Hex.DensePoly.Fraction.size_map {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] [Fraction.NonzeroOne R] (p : DensePoly R) :
    (map p).size = p.size

    Fraction embedding preserves the normalized dense size.

    source
    @[simp]
    theorem Hex.DensePoly.Fraction.leadingCoeff_map {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] [Fraction.NonzeroOne R] (p : DensePoly R) :
    (map p).leadingCoeff = Fraction.ofCoeff p.leadingCoeff

    Fraction embedding preserves the leading coefficient.

    source
    theorem Hex.DensePoly.Fraction.map_eq_zero_iff {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] [Fraction.NonzeroOne R] (p : DensePoly R) :
    map p = 0 ↔ p = 0

    Fraction embedding reflects polynomial zero.

    source
    theorem Hex.DensePoly.Fraction.map_injective {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] [Fraction.NonzeroOne R] {p q : DensePoly R} (h : map p = map q) :
    p = q

    Fraction embedding is injective.

    source
    @[simp]
    theorem Hex.DensePoly.Fraction.map_zero {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] [Fraction.NonzeroOne R] :
    map 0 = 0

    Fraction embedding preserves zero.

    source
    @[simp]
    theorem Hex.DensePoly.Fraction.map_C {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] [Fraction.NonzeroOne R] (a : R) :
    map (C a) = C (Fraction.ofCoeff a)

    Fraction embedding preserves constants.

    source
    @[simp]
    theorem Hex.DensePoly.Fraction.map_add {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] [Fraction.NonzeroOne R] (p q : DensePoly R) :
    map (p + q) = map p + map q

    Fraction embedding preserves addition.

    source
    @[simp]
    theorem Hex.DensePoly.Fraction.map_neg {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] [Fraction.NonzeroOne R] (p : DensePoly R) :
    map (-p) = -map p

    Fraction embedding preserves negation.

    source
    @[simp]
    theorem Hex.DensePoly.Fraction.map_sub {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] [Fraction.NonzeroOne R] (p q : DensePoly R) :
    map (p - q) = map p - map q

    Fraction embedding preserves subtraction.

    source
    @[simp]
    theorem Hex.DensePoly.Fraction.map_scale {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] [Fraction.NonzeroOne R] (a : R) (p : DensePoly R) :
    map (scale a p) = scale (Fraction.ofCoeff a) (map p)

    Fraction embedding preserves scalar multiplication.

    source
    @[simp]
    theorem Hex.DensePoly.Fraction.map_mul {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] [Fraction.NonzeroOne R] (p q : DensePoly R) :
    map (p * q) = map p * map q

    Fraction embedding preserves polynomial multiplication.

    source
    theorem Hex.DensePoly.Fraction.map_pseudoDivMod {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] [Fraction.NonzeroOne R] (f g : DensePoly R) (hg : g ≠ 0) (hgf : g.size ≤ f.size) :
    (map f).pseudoDivMod (map g) = (map (f.pseudoDivMod g).fst, map (f.pseudoDivMod g).snd)

    Pseudo-division commutes with the fraction-field embedding on an ordered nonzero input pair.

    source
    theorem Hex.DensePoly.Fraction.divScalar_pullback {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] [Fraction.NonzeroOne R] (p q : DensePoly R) {b : R} (hb : b ≠ 0) (h : map q = (map p).divScalar (Fraction.ofCoeff b)) :
    p.divScalar b = q

    Pull coefficientwise exact scalar division back from the fraction field.

    The image hypothesis is the integrality certificate later supplied by a generalized subresultant minor.

    source
    theorem Hex.DensePoly.Fraction.divScalar_exact {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] [Fraction.NonzeroOne R] (p : DensePoly R) {b : R} (hb : b ≠ 0) (h : ∀ (n : Nat), ∃ (c : R), Fraction.ofCoeff c = Fraction.ofCoeff (p.coeff n) / Fraction.ofCoeff b) :
    p = scale b (p.divScalar b)

    Coefficientwise integrality in the fraction field proves that executable scalar division reconstructs the original polynomial.