PolynomialLineFlags.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The exact cleared polynomial flags for an internal line system

def OAI.Ostmann.lineTestPolynomials line 16
Source documentation
The distinguished row supplies the coefficient tests; its minors with all other rows supply the rank tests.
```
def lineTestPolynomials {σ J : Type*} (L : J → PolynomialGiantLine σ) (i : J) :
    Bool ⊕ J → MvPolynomial σ ℤ
  | .inl false => (L i).a
  | .inl true => (L i).b
  | .inr j => (L i).minor (L j)
```
Mentions: OAI.Ostmann.PolynomialGiantLine
def OAI.Ostmann.lineFeasibleFlags line 22
theorem OAI.Ostmann.external_polynomialLine_flags_iff line 26
theorem OAI.Ostmann.unit_polynomialLine_flags_iff line 39

theorem OAI.Ostmann.line_divisibility_flags_eq line 57

Source documentation

The divisibility flags of the actual integer evaluations agree exactly with zero tests in the prime residue field.

theorem line_divisibility_flags_eq {J A : Type*} {n : ℕ} (value : A → ℤ)
    (L : J → PolynomialGiantLine (Fin n)) (i : J) (x : Fin n → A) (p : ℕ) :
    (fun s => arithmeticTestFlag (p ∣ (integerTestValue value (lineTestPolynomials L i s) x).natAbs)) =
      (fun s => arithmeticTestFlag
        (MvPolynomial.eval₂Hom (Int.castRingHom (ZMod p))
          (fun j => (value (x j) : ZMod p)) (lineTestPolynomials L i s) = 0)) := by
…

Mentions: OAI.Ostmann.PolynomialGiantLine, OAI.Ostmann.arithmeticTestFlag, OAI.Ostmann.integerTestValue, OAI.Ostmann.lineTestPolynomials