PolynomialGiantTests.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Cleared coefficient and minor tests for the giant lines

structure OAI.Ostmann.PolynomialGiantLine line 11
def OAI.Ostmann.PolynomialGiantRows.numeratorLine line 18
Source documentation
The numerator v * Hminus - w * Hplus, with the ancestor denominator still cleared. The current compensation variable does not occur here.
```
def PolynomialGiantRows.numeratorLine {σ : Type*} (T : PolynomialGiantRows σ)
    (v w : MvPolynomial σ ℤ) : PolynomialGiantLine σ :=
…
```
Mentions: OAI.Ostmann.PolynomialGiantRows, OAI.Ostmann.PolynomialGiantLine
def OAI.Ostmann.PolynomialGiantLine.normalized line 26
def OAI.Ostmann.PolynomialGiantLine.minor line 30
theorem OAI.Ostmann.PolynomialGiantLine.normalized_zero_iff line 32
theorem OAI.Ostmann.PolynomialGiantLine.normalized_minor line 38
theorem OAI.Ostmann.PolynomialGiantLine.normalized_minor_zero_iff line 47

theorem OAI.Ostmann.PolynomialGiantRows.normalized_numeratorLine line 58

Source documentation

Normalizing the cleared numerator gives its actual two coefficients.

theorem PolynomialGiantRows.normalized_numeratorLine {σ K : Type*} [Field K]
    (T : PolynomialGiantRows σ) (v w : MvPolynomial σ ℤ)
    (φ : MvPolynomial σ ℤ →+* K) (hd : φ T.denominator ≠ 0) :
    (T.numeratorLine v w).normalized φ =
      (φ v * (T.normalized φ).c - φ w * (T.normalized φ).a,
        φ v * (T.normalized φ).d - φ w * (T.normalized φ).b) := by
…

Mentions: OAI.Ostmann.PolynomialGiantRows, OAI.Ostmann.PolynomialGiantRows.normalized

theorem OAI.Ostmann.integerPolynomial_cast_eval line 70

Source documentation

Reduction of an integer polynomial evaluation commutes with casting to a prime residue ring. Thus these tests are genuine integer divisibility tests.

theorem integerPolynomial_cast_eval {σ : Type*} (x : σ → ℤ) (F : MvPolynomial σ ℤ) (p : ℕ) :
    ((MvPolynomial.eval₂Hom (RingHom.id ℤ) x F : ℤ) : ZMod p) =
      MvPolynomial.eval₂Hom (Int.castRingHom (ZMod p)) (fun i => (x i : ZMod p)) F := by
…

theorem OAI.Ostmann.integerPolynomial_mod_zero_iff line 78

Source documentation

A cleared polynomial vanishes in the prime field exactly when the prime divides its actual integer evaluation.

theorem integerPolynomial_mod_zero_iff {σ : Type*} (x : σ → ℤ)
    (F : MvPolynomial σ ℤ) (p : ℕ) :
    MvPolynomial.eval₂Hom (Int.castRingHom (ZMod p)) (fun i => (x i : ZMod p)) F = 0 ↔
      (p : ℤ) ∣ MvPolynomial.eval₂Hom (RingHom.id ℤ) x F := by
…