mathlib3 documentation

algebra.order.monoid.nat_cast

Order of numerials in an add_monoid_with_one. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem lt_add_one {α : Type u_1} [has_one α] [add_zero_class α] [partial_order α] [zero_le_one_class α] [ne_zero 1] [covariant_class α α has_add.add has_lt.lt] (a : α) :
a < a + 1
theorem lt_one_add {α : Type u_1} [has_one α] [add_zero_class α] [partial_order α] [zero_le_one_class α] [ne_zero 1] [covariant_class α α (function.swap has_add.add) has_lt.lt] (a : α) :
a < 1 + a
@[simp]

See zero_lt_two' for a version with the type explicit.

@[simp]

See zero_lt_three' for a version with the type explicit.

@[simp]

See zero_lt_four' for a version with the type explicit.

See zero_lt_two for a version with the type implicit.

See zero_lt_three for a version with the type implicit.

See zero_lt_four for a version with the type implicit.