Theorem zero_le_two
Modification history
2024-10-24 21:25
Mathlib/Algebra/Order/Monoid/NatCast.lean
feat: use aliases for `CovariantClass α α (· * ·) (· ≤ ·)` etc (#13154)
Modified zero_le_twoView on Github →2022-12-08 07:28
test/nontriviality.lean
feat: port Algebra.Order.[Ring|Field].Defs (#905) …
Deleted zero_le_twoView on Github →