OAI/NumberTheory/Ostmann/Arithmetic/MovingOutsideResidues.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingSignedOutsideUnits line 10
2. theorem OAI.Ostmann.movingSignedAuxiliaryUnits_split line 18
3. def OAI.Ostmann.movingModularGiantUnits line 32
4. theorem OAI.Ostmann.movingModularGiantUnits_local line 40
5. theorem OAI.Ostmann.movingSignedOutsideUnits_modular line 47
6. theorem OAI.Ostmann.movingModularSpectator_nonzero_units line 63

   Source documentation

   With the original zero convention, a nonzero spectator coefficient already enforces every outside giant-unit test at that prime.

   theorem movingModularSpectator_nonzero_units {σ : Type*} (value : σ → ℕ)
       (q : ℕ) [Fact q.Prime] (g : ZMod q → ℂ) (D : (ZMod q)ˣ) (hg0 : g 0 = 0)
       {n : ℕ} (T : MovingSlotData σ n) (x y : ZMod q)
       (h : movingModularSpectator value q g D T x y ≠ 0) :
       movingModularGiantUnits value q T x y := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingModularSpectator, OAI.Ostmann.movingModularGiantUnits

7. theorem OAI.Ostmann.movingSignedOutsideUnits_mul line 92
8. theorem OAI.Ostmann.movingSignedOutsideUnits_one line 102
9. theorem OAI.Ostmann.movingSignedOutsideUnits_list line 109
10. theorem OAI.Ostmann.movingModularSpectatorProduct_outside_units line 120