OAI/NumberTheory/Ostmann/Supply/GroupedPrimitiveCharactersLift.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Supply.GroupedPrimitiveCharacters.modulus line 10
2. theorem OAI.Ostmann.Supply.GroupedPrimitiveCharacters.dvd_modulus line 13
3. instance OAI.Ostmann.Supply.GroupedPrimitiveCharacters.modulus_neZero line 16
4. def OAI.Ostmann.Supply.GroupedPrimitiveCharacters.localLift line 22
5. def OAI.Ostmann.Supply.GroupedPrimitiveCharacters.fullCharacter line 26
6. def OAI.Ostmann.Supply.GroupedPrimitiveCharacters.fullCharacterHom line 29
7. theorem OAI.Ostmann.Supply.GroupedPrimitiveCharacters.fullCharacter_div line 36
8. theorem OAI.Ostmann.Supply.GroupedPrimitiveCharacters.mulChar_prod_apply_unit line 40
9. theorem OAI.Ostmann.Supply.GroupedPrimitiveCharacters.fullCharacter_apply_unit line 47
10. theorem OAI.Ostmann.Supply.GroupedPrimitiveCharacters.fullCharacter_apply_nat line 56