OAI/Algebra/GroupRing/RelationArea.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.TorsionFreeZeroDivisors.RelationArea.G line 15
  2. abbrev OAI.TorsionFreeZeroDivisors.RelationArea.N line 16
  3. abbrev OAI.TorsionFreeZeroDivisors.RelationArea.q line 17
  4. def OAI.TorsionFreeZeroDivisors.RelationArea.term line 18
  5. def OAI.TorsionFreeZeroDivisors.RelationArea.total line 21
  6. lemma OAI.TorsionFreeZeroDivisors.RelationArea.total_append line 22
  7. lemma OAI.TorsionFreeZeroDivisors.RelationArea.total_reverse_flip line 24
  8. lemma OAI.TorsionFreeZeroDivisors.RelationArea.total_eq line 31
  9. def OAI.TorsionFreeZeroDivisors.RelationArea.area line 39
  10. lemma OAI.TorsionFreeZeroDivisors.RelationArea.area_eq line 41
  11. lemma OAI.TorsionFreeZeroDivisors.RelationArea.area_mul line 45
  12. lemma OAI.TorsionFreeZeroDivisors.RelationArea.area_one line 51
  13. def OAI.TorsionFreeZeroDivisors.RelationArea.conjugate line 54
  14. def OAI.TorsionFreeZeroDivisors.RelationArea.move line 56
  15. lemma OAI.TorsionFreeZeroDivisors.RelationArea.move_mk line 58
  16. lemma OAI.TorsionFreeZeroDivisors.RelationArea.move_word line 63
  17. lemma OAI.TorsionFreeZeroDivisors.RelationArea.move_term line 72
  18. lemma OAI.TorsionFreeZeroDivisors.RelationArea.move_total line 76
  19. lemma OAI.TorsionFreeZeroDivisors.RelationArea.area_conjugate line 80
  20. def OAI.TorsionFreeZeroDivisors.RelationArea.d₂ line 86
  21. lemma OAI.TorsionFreeZeroDivisors.RelationArea.d₂_single line 88
  22. lemma OAI.TorsionFreeZeroDivisors.RelationArea.d₂_translate line 91
  23. lemma OAI.TorsionFreeZeroDivisors.RelationArea.q_rel line 97
  24. lemma OAI.TorsionFreeZeroDivisors.RelationArea.q_word line 98
  25. lemma OAI.TorsionFreeZeroDivisors.RelationArea.fox_conjugate line 100
  26. lemma OAI.TorsionFreeZeroDivisors.RelationArea.d₂_term line 104
  27. lemma OAI.TorsionFreeZeroDivisors.RelationArea.d₂_total line 110
  28. lemma OAI.TorsionFreeZeroDivisors.RelationArea.d₂_area line 120
  29. lemma OAI.TorsionFreeZeroDivisors.RelationArea.boundary_d₂ line 122