Theorem symm_toLexMulEquiv

Modification history

2025-08-09 19:44

Mathlib/Algebra/Order/Group/Equiv.lean

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

Added symm_toLexMulEquiv View on Github →