OAI/Algebra/OddKaplansky/CosetCoordinates.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OddKaplansky.CosetCoordinates.rep line 12
2. lemma OAI.OddKaplansky.CosetCoordinates.rep_mk line 13
3. lemma OAI.OddKaplansky.CosetCoordinates.residue_mem line 14
4. def OAI.OddKaplansky.CosetCoordinates.residue line 16
5. lemma OAI.OddKaplansky.CosetCoordinates.reconstruct line 17
6. lemma OAI.OddKaplansky.CosetCoordinates.mk_rep_mul line 18
7. lemma OAI.OddKaplansky.CosetCoordinates.residue_rep_mul line 20
8. def OAI.OddKaplansky.CosetCoordinates.equiv line 24
9. lemma OAI.OddKaplansky.CosetCoordinates.equiv_symm_apply line 29
10. lemma OAI.OddKaplansky.CosetCoordinates.sum_right_invariant line 32
11. lemma OAI.OddKaplansky.CosetCoordinates.sum_left_invariant line 37
12. lemma OAI.OddKaplansky.CosetCoordinates.coprime_order_of_sum line 44
13. lemma OAI.OddKaplansky.CosetCoordinates.eq_one_of_power_and_sum line 62