Theorem symm_ofLexLinearEquiv

Modification history

2025-08-09 19:44

Mathlib/Algebra/Order/Module/Equiv.lean

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

Added symm_ofLexLinearEquiv View on Github →