OAI/NumberTheory/Ostmann/Arithmetic/MovingTemplateEnumeration.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingTemplateSlotList_nodup line 12
2. def OAI.Ostmann.movingTemplateListEquiv line 28
3. theorem OAI.Ostmann.movingTemplateListEquiv_apply line 33
4. theorem OAI.Ostmann.movingTemplate_multiplier_list line 38

   Source documentation

   Enumerating the full template does not change its masked cofactor product.

   theorem movingTemplate_multiplier_list {A : Type*} (value : A → ℕ)
       (hprime : ∀ a, (value a).Prime) (n r m : ℕ)
       (x : MovingRegularSlot n r m → A) (active : MovingRegularSlot n r m → Bool)
       (g : ∀ q : ℕ, ZMod q → ℂ) (D XL XR : ℕ) (s : ℤ) :
       let L := movingTemplateSlotList n r m
   …

   Mentions: OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.movingTemplateSlotList