OAI/NumberTheory/Ostmann/Characters/PolynomialAncestorNonvanishing.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.polynomialAncestorRows_denominator_ne_zero line 9
2. theorem OAI.Ostmann.polynomialAncestorRows_normalized_isUnit_det line 25
3. theorem OAI.Ostmann.polynomialAncestorRows_numeratorLine_nonzero line 44

   Source documentation

   Every occurrence numerator formed after these actual reversals is nonzero in the prime field. The current compensation variable is absent.

   theorem polynomialAncestorRows_numeratorLine_nonzero {σ K : Type*} [Field K]
       (steps : List (PolynomialReversal σ)) (φ : MvPolynomial σ ℤ →+* K)
       (h : ∀ s ∈ steps, φ s.v ≠ 0 ∧ φ s.w ≠ 0 ∧ φ s.u ≠ 0)
       (v w : MvPolynomial σ ℤ) (hv : φ v ≠ 0) (hw : φ w ≠ 0) :
       (((polynomialAncestorRows steps).numeratorLine v w).normalized φ).1 ≠ 0 ∨
         (((polynomialAncestorRows steps).numeratorLine v w).normalized φ).2 ≠ 0 := by
   …

   Mentions: OAI.Ostmann.PolynomialReversal, OAI.Ostmann.polynomialAncestorRows