OAI/NumberTheory/Ostmann/Supply/GroupedPrimitiveCharacters.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Supply.GroupedPrimitiveCharacters.PrimitivePair line 9
2. def OAI.Ostmann.Supply.GroupedPrimitiveCharacters.principalPair line 11
3. def OAI.Ostmann.Supply.GroupedPrimitiveCharacters.inducePair line 14
4. def OAI.Ostmann.Supply.GroupedPrimitiveCharacters.primitivePair line 19
5. theorem OAI.Ostmann.Supply.GroupedPrimitiveCharacters.inducePair_primitivePair line 24
6. theorem OAI.Ostmann.Supply.GroupedPrimitiveCharacters.primitivePair_injective line 32
7. theorem OAI.Ostmann.Supply.GroupedPrimitiveCharacters.primitivePair_fst line 38
8. theorem OAI.Ostmann.Supply.GroupedPrimitiveCharacters.primitivePair_pos line 45
9. theorem OAI.Ostmann.Supply.GroupedPrimitiveCharacters.primitivePair_apply_nat line 49
10. theorem OAI.Ostmann.Supply.GroupedPrimitiveCharacters.pair_eq_principal_of_fst_eq_one line 62
11. theorem OAI.Ostmann.Supply.GroupedPrimitiveCharacters.primitivePair_one line 73
12. theorem OAI.Ostmann.Supply.GroupedPrimitiveCharacters.primitivePair_eq_principal_iff line 80