Commit 2023-04-02 23:34 8882e05a

View on Github →

chore: Golf algebra.order.lattice_group (#2478) Match https://github.com/leanprover-community/mathlib/pull/18046

Estimated changes

Modified Mathlib/Algebra/Order/LatticeGroup.lean

modified theorem LatticeOrderedCommGroup.mabs_of_one_le

modified theorem LatticeOrderedCommGroup.neg_eq_one_iff'

modified theorem LatticeOrderedCommGroup.neg_of_le_one

modified theorem LatticeOrderedCommGroup.pos_eq_neg_inv

modified theorem LatticeOrderedCommGroup.pos_eq_one_iff

added theorem inf_mul

modified theorem mul_inf

modified theorem mul_sup

added theorem sup_mul