Theorem WithZero.zero_lt_coe

Modification history

2024-03-28 11:53

Mathlib/Algebra/Order/Monoid/WithZero.lean

chore: Reduce scope of `LinearOrderedCommGroupWithZero` (#11716) …

Modified WithZero.zero_lt_coe View on Github →

2022-12-06 13:59

Mathlib/Algebra/Order/Monoid/WithZero/Defs.lean

feat: port Algebra.Order.Monoid.WithZero (#851) …

Added WithZero.zero_lt_coe View on Github →