OAI/NumberTheory/Ostmann/Characters/TemplateAmplitudeRecurrenceSupportPropagationBasic.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Ostmann.Characters.Template.sourceState_copied_value line 12
2. lemma OAI.Ostmann.Characters.Template.sourceState_outside_value line 17
3. lemma OAI.Ostmann.Characters.Template.CurrentAtomSupport.copied_pos line 22
4. lemma OAI.Ostmann.Characters.Template.CurrentAtomSupport.outside_pos line 27
5. lemma OAI.Ostmann.Characters.Template.CurrentAtomSupport.copied_pairwise line 32
6. lemma OAI.Ostmann.Characters.Template.CurrentAtomSupport.outside_pairwise line 39
7. lemma OAI.Ostmann.Characters.Template.CurrentAtomSupport.copied_outside_coprime line 46
8. lemma OAI.Ostmann.Characters.Template.CurrentAtomSupport.copied_pivot_coprime line 55
9. lemma OAI.Ostmann.Characters.Template.coprime_cross_of_reversal line 67
10. lemma OAI.Ostmann.Characters.Template.isCoprime_of_prime_factors_large line 77