OAI/Algebra/OddKaplansky/AugmentBound.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OddKaplansky.LocalAlgebra.X line 15
2. lemma OAI.OddKaplansky.LocalAlgebra.X_nil line 17
3. def OAI.OddKaplansky.LocalAlgebra.exponentModule line 21
4. def OAI.OddKaplansky.LocalAlgebra.differenceSubgroup line 25
5. def OAI.OddKaplansky.LocalAlgebra.generatorIdeal line 44
6. lemma OAI.OddKaplansky.LocalAlgebra.generator_mem line 46
7. lemma OAI.OddKaplansky.LocalAlgebra.difference_mem line 69
8. lemma OAI.OddKaplansky.LocalAlgebra.scalar_difference_mem line 81
9. lemma OAI.OddKaplansky.LocalAlgebra.ker_le_generator line 94
10. lemma OAI.OddKaplansky.NilpotentSum.bounded line 107
11. lemma OAI.OddKaplansky.LocalAlgebra.generator_nil line 127
12. lemma OAI.OddKaplansky.LocalAlgebra.kernel_nil_of_basis line 134
13. lemma OAI.OddKaplansky.LocalAlgebra.dimension_le_three line 141
14. lemma OAI.OddKaplansky.LocalAlgebra.kernel_nil_three line 159