Theorem coe_ofLexLinearEquiv

Modification history

2025-08-09 19:44

Mathlib/Algebra/Order/Module/Equiv.lean

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

Added coe_ofLexLinearEquiv View on Github →