Theorem LatticeOrderedCommGroup.abs_inv

Modification history

2023-08-09 22:00
Mathlib/Algebra/Order/LatticeGroup.lean
refactor(Algebra/Order/LatticeGroup): Non-commutative Lattice Groups (#6452) …
Deleted LatticeOrderedCommGroup.abs_invView on Github →
2023-08-04 21:46
Mathlib/Algebra/Order/LatticeGroup.lean
feat(Algebra/Order/LatticeGroup): Add missing `abs_inv` to LatticeGroup (#6357) …
Added LatticeOrderedCommGroup.abs_invView on Github →