OAI/Analysis/Kaplansky/Regular/FreeNormal.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KaplanskyConsequences.Regular.translate line 12
  2. lemma OAI.KaplanskyConsequences.Regular.translate_of line 13
  3. lemma OAI.KaplanskyConsequences.Regular.translate_zero line 15
  4. lemma OAI.KaplanskyConsequences.Regular.translate_add line 19
  5. lemma OAI.KaplanskyConsequences.Regular.translate_one line 23
  6. lemma OAI.KaplanskyConsequences.Regular.translate_neg_one line 24
  7. def OAI.KaplanskyConsequences.Regular.height line 29
  8. def OAI.KaplanskyConsequences.Regular.exponent line 30
  9. lemma OAI.KaplanskyConsequences.Regular.exponent_one line 31
  10. lemma OAI.KaplanskyConsequences.Regular.exponent_mul line 32
  11. lemma OAI.KaplanskyConsequences.Regular.exponent_inv line 33
  12. lemma OAI.KaplanskyConsequences.Regular.exponent_a line 34
  13. lemma OAI.KaplanskyConsequences.Regular.exponent_b line 35
  14. lemma OAI.KaplanskyConsequences.Regular.coordinate_one line 36
  15. lemma OAI.KaplanskyConsequences.Regular.coordinate_a line 37
  16. lemma OAI.KaplanskyConsequences.Regular.coordinate_b line 38
  17. lemma OAI.KaplanskyConsequences.Regular.coordinate_a_inv line 39
  18. lemma OAI.KaplanskyConsequences.Regular.coordinate_b_inv line 40
  19. lemma OAI.KaplanskyConsequences.Regular.action_affine line 42
  20. lemma OAI.KaplanskyConsequences.Regular.coordinate_mul line 63
  21. def OAI.KaplanskyConsequences.Regular.genZ line 68
  22. def OAI.KaplanskyConsequences.Regular.kernelMap line 69
  23. lemma OAI.KaplanskyConsequences.Regular.kernelMap_of line 70
  24. lemma OAI.KaplanskyConsequences.Regular.kernelMap_translate line 71
  25. lemma OAI.KaplanskyConsequences.Regular.normal_form line 79
  26. lemma OAI.KaplanskyConsequences.Regular.coordinate_exponent_separate line 96
  27. lemma OAI.KaplanskyConsequences.Regular.action_genZ line 99
  28. lemma OAI.KaplanskyConsequences.Regular.exponent_genZ line 123
  29. lemma OAI.KaplanskyConsequences.Regular.coordinate_genZ line 125
  30. lemma OAI.KaplanskyConsequences.Regular.coordinate_genZ_mul line 127