Commit 2023-08-09 22:00 cdd51dd5

View on Github →

refactor(Algebra/Order/LatticeGroup): Non-commutative Lattice Groups (#6452) Generalise results in Algebra/Order/LatticeGroup to the case where the group is non-commutative

Estimated changes

modified theorem inf_mul
modified theorem inv_inf_eq_sup_inv
modified theorem inv_sup_eq_inv_inf_inv
modified theorem sup_mul