Theorem zero_lt_one

Modification history

2022-12-07 15:11

Mathlib/Algebra/Order/ZeroLEOne.lean

port: Algebra.Order.Monoid.NatCast (#893) …

Modified zero_lt_one View on Github →

2022-11-28 22:26

Mathlib/Tactic/Linarith/Lemmas.lean

feat: port linarith (#526) …

Added zero_lt_one View on Github →