Theorem zero_le'

Modification history

2026-05-06 19:54

Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

feat: `IsBotOneClass` and `IsBotZeroClass` (#38730) …

Deleted zero_le'View on Github →

2026-01-08 11:26

Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

refactor: make `LinearOrderedCommMonoidWithZero`s cancellative (#31749) …

Modified zero_le'View on Github →

2024-03-28 11:53

Mathlib/Algebra/Order/Monoid/WithZero.lean

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

Modified zero_le'View on Github →

2022-12-12 09:20

Mathlib/Algebra/Order/WithZero.lean

feat: port Algebra.Order.WithZero (#903) …

Added zero_le'View on Github →