OAI/Analysis/Kaplansky/Regular/FreeFamily.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KaplanskyConsequences.Regular.FZ line 13
  2. def OAI.KaplanskyConsequences.Regular.shift line 15
  3. def OAI.KaplanskyConsequences.Regular.action line 17
  4. def OAI.KaplanskyConsequences.Regular.a line 20
  5. def OAI.KaplanskyConsequences.Regular.b line 21
  6. def OAI.KaplanskyConsequences.Regular.freeGen line 23
  7. lemma OAI.KaplanskyConsequences.Regular.action_a line 27
  8. lemma OAI.KaplanskyConsequences.Regular.action_b line 28
  9. lemma OAI.KaplanskyConsequences.Regular.shift_of line 29
  10. lemma OAI.KaplanskyConsequences.Regular.action_freeGen line 32
  11. def OAI.KaplanskyConsequences.Regular.coordinate line 41
  12. lemma OAI.KaplanskyConsequences.Regular.coordinate_freeGen_mul line 43
  13. def OAI.KaplanskyConsequences.Regular.Prefix line 47
  14. lemma OAI.KaplanskyConsequences.Regular.prefix_disjoint line 50
  15. lemma OAI.KaplanskyConsequences.Regular.prefix_mul_of_not_negative line 55
  16. lemma OAI.KaplanskyConsequences.Regular.positive_of_not_negative_inverse line 72