TransferIntegerPhases.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Reducing the actual integer transfer equation at each surviving prime

theorem OAI.Ostmann.transfer_equation_mod_left line 11
Source documentation
A left-slot prime divides the left product, so its local equation loses that term. No primality is required for this algebraic reduction.
```
theorem transfer_equation_mod_left (p L R M : ℕ) (v w s : ℤ)
    (hpL : p ∣ L) (h : v * R - w * L = s * M) :
    (v : ZMod p) * (R : ZMod p) = (s : ZMod p) * (M : ZMod p) := by
…
```
theorem OAI.Ostmann.transfer_equation_mod_right line 21
theorem OAI.Ostmann.transfer_equation_mod_outside line 31
theorem OAI.Ostmann.zmod_natCast_ne_zero_of_coprime line 40
Source documentation
Natural coprimality supplies the nonzero denominators in the prime field.
```
theorem zmod_natCast_ne_zero_of_coprime {p : ℕ} [Fact p.Prime] (a : ℕ)
    (h : a.Coprime p) : (a : ZMod p) ≠ 0 :=
…
```

theorem OAI.Ostmann.transfer_left_additive_integer line 45

Source documentation

The actual integer equation supplies the left additive phase identity.

theorem transfer_left_additive_integer {p : ℕ} [Fact p.Prime]
    (L R M D : ℕ) (v w s : ℤ) (t : ZMod p)
    (hpL : p ∣ L) (hM : M.Coprime p) (hR : R.Coprime p) (hD : D.Coprime p)
    (hrel : v * R - w * L = s * M) :
    ZMod.stdAddChar (t * ((v : ZMod p) / ((M : ZMod p) * (D : ZMod p)))) =
      ZMod.stdAddChar (t * ((s : ZMod p) / ((R : ZMod p) * (D : ZMod p)))) :=
…

theorem OAI.Ostmann.transfer_right_additive_integer line 58

Source documentation

The right copy is conjugated before using the integer equation.

theorem transfer_right_additive_integer {p : ℕ} [Fact p.Prime]
    (L R M D : ℕ) (v w s : ℤ) (t : ZMod p)
    (hpR : p ∣ R) (hM : M.Coprime p) (hL : L.Coprime p) (hD : D.Coprime p)
    (hrel : v * R - w * L = s * M) :
    star (ZMod.stdAddChar (t * ((w : ZMod p) / ((M : ZMod p) * (D : ZMod p))))) =
      ZMod.stdAddChar (t * ((s : ZMod p) / ((L : ZMod p) * (D : ZMod p)))) :=
…