Commit 2025-08-09 19:44 8afc93b4

View on Github →

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

Estimated changes

added theorem coe_ofLexMulEquiv
added theorem coe_toLexMulEquiv
added def ofLexMulEquiv
added theorem symm_ofLexMulEquiv
added theorem symm_toLexMulEquiv
added theorem toEquiv_ofLexMulEquiv
added theorem toEquiv_toLexMulEquiv
added def toLexMulEquiv
deleted theorem coe_symm_toLexMulEquiv
deleted theorem coe_toLexMulEquiv
deleted theorem toEquiv_toLexMulEquiv
deleted def toLexMulEquiv
added theorem coe_ofLexLinearEquiv
added theorem coe_toLexLinearEquiv
added def ofLexLinearEquiv
added theorem symm_ofLexLinearEquiv
added theorem symm_toLexLinearEquiv
added def toLexLinearEquiv