OAI/Algebra/OddKaplansky/ModularSource.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OddKaplansky.Augmentation.regular_translation line 15
2. abbrev OAI.OddKaplansky.ModularSource.P line 29
3. lemma OAI.OddKaplansky.ModularSource.card_P line 30
4. lemma OAI.OddKaplansky.ModularSource.base_nonzero line 31
5. lemma OAI.OddKaplansky.ModularSource.quartic_large line 52
6. lemma OAI.OddKaplansky.ModularSource.left_ann line 60
7. lemma OAI.OddKaplansky.ModularSource.right_ann line 75
8. lemma OAI.OddKaplansky.ModularSource.high_small line 90
9. lemma OAI.OddKaplansky.ModularSource.point_small line 94
10. lemma OAI.OddKaplansky.ModularSource.high_large line 98
11. lemma OAI.OddKaplansky.ModularSource.exists_idempotent line 102