OAI/NumberTheory/Ostmann/Characters/TemplateOneSidedSupportTelescopingFinite.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Characters.TemplateOneSidedSupportTelescoping.hybridSupport line 11
2. def OAI.Ostmann.Characters.TemplateOneSidedSupportTelescoping.remainder line 15
3. def OAI.Ostmann.Characters.TemplateOneSidedSupportTelescoping.hybridValue line 19
4. theorem OAI.Ostmann.Characters.TemplateOneSidedSupportTelescoping.hybridSupport_iff_remainder line 23
5. theorem OAI.Ostmann.Characters.TemplateOneSidedSupportTelescoping.hybridSupport_insert_iff line 37
6. theorem OAI.Ostmann.Characters.TemplateOneSidedSupportTelescoping.norm_telescope_finset line 53