Theorem toEquiv_toLexMulEquiv

Modification history

2025-08-09 19:44

Mathlib/Algebra/Order/Group/Equiv.lean

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

Modified toEquiv_toLexMulEquiv View on Github →

2025-06-16 16:23

Mathlib/Algebra/Order/GroupWithZero/Lex.lean

feat(Algebra/Order/{Monoid,GroupWithZero}/Lex): ordered inclusions and projections of prod of ordered groups (#22420)

Added toEquiv_toLexMulEquiv View on Github →