Theorem one_lt_two
Modification history
2022-12-06 04:12
src/algebra/order/monoid/nat_cast.lean
move(algebra/order/monoid/*): relocate `zero_le_one_class` again (#17820) …
Modified one_lt_twoView on Github →2022-12-04 17:00
src/algebra/order/monoid/with_zero/defs.lean
feat(algebra/order/zero_le_one): generalize lemmas (#17465) …
Modified one_lt_twoView on Github →2022-10-08 09:14
src/algebra/order/ring.lean
feat(algebra/order/ring): Non-cancellative ordered semirings (#16172) …
Modified one_lt_twoView on Github →2020-06-08 15:06
src/algebra/ordered_ring.lean
chore(algebra/ordered_ring): use le instead of ge (#2986)
Modified one_lt_twoView on Github →2018-01-14 21:59
algebra/ordered_ring.lean
feat(algebra/field): more division lemmas
Modified one_lt_twoView on Github →2017-09-28 19:16
algebra/ordered_ring.lean
chore(topology): move general theorems to the corresponding theories
Modified one_lt_twoView on Github →2017-09-21 13:22
topology/real.lean
feat(topology/lebesgue_measure): add Lebesgue outer measure; show that the lower half open interval is measurable
Modified one_lt_twoView on Github →2017-09-21 10:33
topology/real.lean
Merge branch 'master' of https://github.com/leanprover/mathlib
Modified one_lt_twoView on Github →