OAI/NumberTheory/Ostmann/Quadratic/CommonCenterReduction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Reducing the common rational center and transporting its congruences

  1. theorem OAI.Ostmann.exists_reduced_commonCenter line 12
  2. theorem OAI.Ostmann.reduced_commonCenter_mod_prime line 29

    Source documentation

    The common lift gives the same field center after reducing the rational number.

    theorem reduced_commonCenter_mod_prime (n h : ℤ) (a m p : ℕ)
    [Fact p.Prime] (ha : 0 < a) (hap : a < p) (hm : 0 < m) (hma : m ≤ a)
    (heq : n * (m : ℤ) = (a : ℤ) * h) (t : ℤ)
    (hcong : (p : ℤ) ∣ n - (a : ℤ) * t) :
    (t : ZMod p) = (h : ZMod p) / (m : ZMod p) := by
…