Theorem toEquiv_ofLexMulEquiv

Modification history

2025-08-09 19:44

Mathlib/Algebra/Order/Group/Equiv.lean

feat(Algebra/Order): `LinearEquiv` version of `toLex`/`ofLex` (#27711)

Added toEquiv_ofLexMulEquiv View on Github →