OAI/NumberTheory/Ostmann/Construction/InitialEtaCRTBasic.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Construction.InitialEta.crtTail line 14
2. abbrev OAI.Ostmann.Construction.InitialEta.StatePosition line 16
3. def OAI.Ostmann.Construction.InitialEta.stateModuli line 18
4. def OAI.Ostmann.Construction.InitialEta.stateLocalTest line 21
5. theorem OAI.Ostmann.Construction.InitialEta.stateModuli_ofFn line 27
6. theorem OAI.Ostmann.Construction.InitialEta.stateModuli_prod line 32
7. theorem OAI.Ostmann.Construction.InitialEta.stateModuli_prime line 37
8. theorem OAI.Ostmann.Construction.InitialEta.stateModuli_pairwise line 45
9. theorem OAI.Ostmann.Construction.InitialEta.state_coprime_of_distinct line 57
10. theorem OAI.Ostmann.Construction.InitialEta.otherProduct_eq_div line 64
11. def OAI.Ostmann.Construction.InitialEta.statePhysicalProduct line 69
12. theorem OAI.Ostmann.Construction.InitialEta.stateLocalTest_product line 76