OAI/NumberTheory/Ostmann/Characters/TemplateOneSidedSupportTelescopingPairLiteral.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Characters.TemplateOneSidedSupportTelescoping.retained_pair_eq_indicator line 15
2. theorem OAI.Ostmann.Characters.TemplateOneSidedSupportTelescoping.core_pair_eq_indicator line 30
3. theorem OAI.Ostmann.Characters.TemplateOneSidedSupportTelescoping.core_pair_fixed_gate line 45
4. theorem OAI.Ostmann.Characters.TemplateOneSidedSupportTelescoping.sampled_prime_transfer_iff line 63
5. theorem OAI.Ostmann.Characters.TemplateOneSidedSupportTelescoping.retained_prime_pair_eq_sampled line 77