Theorem OrderMonoidHom.inlₗ_mul_inrₗ_eq_toLex

Modification history

2025-06-16 16:23

Mathlib/Algebra/Order/Monoid/Lex.lean

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

Added OrderMonoidHom.inlₗ_mul_inrₗ_eq_toLex View on Github →