Theorem LinearOrderedCommGroupWithZero.inl_mul_inr_eq_coe_toLex

Modification history

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 LinearOrderedCommGroupWithZero.inl_mul_inr_eq_coe_toLexView on Github →