OAI/Analysis/JiangSu/CuntzSemigroup/SemigroupGrothendieck.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Pureness.OrderedSemigroup.grothendieck_eq_iff line 18
  2. theorem OAI.Pureness.OrderedSemigroup.grothendieck_difference_eq_iff line 25
  3. theorem OAI.Pureness.OrderedSemigroup.grothendieck_exists_difference line 32
  4. def OAI.Pureness.OrderedSemigroup.grothendieckCone line 42
  5. theorem OAI.Pureness.OrderedSemigroup.grothendieck_mem_cone_iff line 49
  6. lemma OAI.Pureness.OrderedSemigroup.grothendieck_of_nonneg line 64
  7. theorem OAI.Pureness.OrderedSemigroup.grothendieck_orderUnit line 68
  8. abbrev OAI.Pureness.OrderedSemigroup.RationalGroup line 83
  9. instance OAI.Pureness.OrderedSemigroup.rationalGroupModule line 84
  10. abbrev OAI.Pureness.OrderedSemigroup.toRationalGroup line 87
  11. theorem OAI.Pureness.OrderedSemigroup.rationalGroup_eq_iff line 90
  12. theorem OAI.Pureness.OrderedSemigroup.rationalGroup_denominator line 115
  13. theorem OAI.Pureness.RationalRiesz.RieszExtension.step line 167
  14. theorem OAI.Pureness.RationalRiesz.RieszExtension.exists_top line 221
  15. theorem OAI.Pureness.RationalRiesz.riesz_extension line 249