OAI/NumberTheory/Ostmann/ZeroDensity/ZeroVariableHistory.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Removing reconstructed-pivot coprimalities to actual prime slots

  1. def OAI.Ostmann.zeroHistoryVariable line 13
  2. theorem OAI.Ostmann.zeroHistoryVariable_absent line 17
  3. theorem OAI.Ostmann.zeroHistoryVariable_eval line 23
  4. theorem OAI.Ostmann.zeroHistoryVariable_degree line 32
  5. theorem OAI.Ostmann.zeroHistoryVariable_dvd_iff line 59

    Source documentation

    Divisibility by the sampled prime is unchanged on setting that variable to zero in the cleared numerator.

    theorem zeroHistoryVariable_dvd_iff {σ : Type*} (i : σ) (P : MvPolynomial σ ℤ)
    (x : σ → ℤ) (p : ℕ) (hxi : x i = p) :
    p ∣ (MvPolynomial.eval₂Hom (RingHom.id ℤ) x P).natAbs ↔
      p ∣ (MvPolynomial.eval₂Hom (RingHom.id ℤ) x (zeroHistoryVariable i P)).natAbs := by
…

    Mentions: OAI.Ostmann.zeroHistoryVariable

  6. theorem OAI.Ostmann.zeroHistoryVariable_identically_bad line 73
  7. theorem OAI.Ostmann.reconstructed_prime_coprimality_error line 79