OAI/Algebra/OddKaplansky/OrderedCoordinates.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OddKaplansky.OrderedCosetCoordinates.rep line 13
  2. lemma OAI.OddKaplansky.OrderedCosetCoordinates.rep_mk line 14
  3. lemma OAI.OddKaplansky.OrderedCosetCoordinates.rep_le line 17
  4. lemma OAI.OddKaplansky.OrderedCosetCoordinates.rep_injective line 18
  5. def OAI.OddKaplansky.OrderedCosetCoordinates.quotientOrder line 22
  6. lemma OAI.OddKaplansky.OrderedCosetCoordinates.residue_mem line 23
  7. def OAI.OddKaplansky.OrderedCosetCoordinates.residue line 25
  8. lemma OAI.OddKaplansky.OrderedCosetCoordinates.reconstruct line 26
  9. lemma OAI.OddKaplansky.OrderedCosetCoordinates.mk_rep_mul line 27
  10. lemma OAI.OddKaplansky.OrderedCosetCoordinates.residue_rep_mul line 29
  11. def OAI.OddKaplansky.OrderedCosetCoordinates.equiv line 33
  12. lemma OAI.OddKaplansky.OrderedCosetCoordinates.equiv_symm_apply line 38
  13. lemma OAI.OddKaplansky.OrderedCosetCoordinates.sum_right_invariant line 40
  14. lemma OAI.OddKaplansky.OrderedCosetCoordinates.sum_left_invariant line 45
  15. lemma OAI.OddKaplansky.OrderedCosetCoordinates.coprime_order_of_sum line 52
  16. lemma OAI.OddKaplansky.OrderedCosetCoordinates.eq_one_of_power_and_sum line 70