Commit 2024-01-08 13:15 33c5d03b

View on Github →

chore: New file for lattice ordered groups (#9457) Split Algebra.Order.LatticeGroup into two files:

  • Algebra.Order.Group.Lattice for general properties of lattice ordered groups
  • Algebra.Order.Group.PosPart for properties of the positive and negative parts Note that the latter also contains properties of the absolute value. These will be moved to Algebra.Order.Group.Abs in a later PR. Part of #9411

Estimated changes

added theorem div_inf
added theorem div_sup
added theorem inf_div
added theorem inf_mul
added theorem inf_mul_sup
added theorem inv_inf
added theorem inv_sup
added theorem mul_inf
added theorem mul_sup
added theorem pow_two_semiclosed
added theorem sup_div
added theorem sup_mul
deleted theorem inf_mul
deleted theorem inf_mul_sup
deleted theorem inv_inf_eq_sup_inv
deleted theorem inv_sup_eq_inv_inf_inv
deleted theorem mul_inf
deleted theorem mul_sup
deleted theorem sup_mul