Mathlib Changelog
v4
Changelog
About
Github
Def
Prod.Lex.toLexOrderHom
Modification history
2025-06-16 16:23
Mathlib/Order/Prod/Lex/Hom.lean
feat(Algebra/Order/{Monoid,GroupWithZero}/Lex): ordered inclusions and projections of prod of ordered groups (#22420)
Added
Prod.Lex.toLexOrderHom
View on Github →