OAI/GroupTheory/Kervaire/Model.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Kervaire.WordGroup line 9

   Also declared: ComparatorChallenges/Kervaire.lean:11 (same declaration text).

2. def OAI.Kervaire.exponentSum line 11

   Also declared: ComparatorChallenges/Kervaire.lean:13 (same declaration text).

3. def OAI.Kervaire.Unimodular line 14

   Also declared: ComparatorChallenges/Kervaire.lean:16 (same declaration text).

4. def OAI.Kervaire.relatorClosure line 17

   Also declared: ComparatorChallenges/Kervaire.lean:19 (same declaration text).

5. instance OAI.Kervaire.(instance at line 20) line 20
6. abbrev OAI.Kervaire.RelatorQuotient line 23

   Also declared: ComparatorChallenges/Kervaire.lean:25 (same declaration text).

7. def OAI.Kervaire.coefficientMap line 26

   Also declared: ComparatorChallenges/Kervaire.lean:28 (same declaration text).