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 : α) :
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 : α) :
theorem
zero_le_two
{α : Type u_1}
[add_monoid_with_one α]
[preorder α]
[zero_le_one_class α]
[covariant_class α α has_add.add has_le.le] :
0 ≤ 2
theorem
zero_le_three
{α : Type u_1}
[add_monoid_with_one α]
[preorder α]
[zero_le_one_class α]
[covariant_class α α has_add.add has_le.le] :
0 ≤ 3
theorem
zero_le_four
{α : Type u_1}
[add_monoid_with_one α]
[preorder α]
[zero_le_one_class α]
[covariant_class α α has_add.add has_le.le] :
0 ≤ 4
theorem
one_le_two
{α : Type u_1}
[add_monoid_with_one α]
[has_le α]
[zero_le_one_class α]
[covariant_class α α has_add.add has_le.le] :
1 ≤ 2
theorem
one_le_two'
{α : Type u_1}
[add_monoid_with_one α]
[has_le α]
[zero_le_one_class α]
[covariant_class α α (function.swap has_add.add) has_le.le] :
1 ≤ 2
@[simp]
theorem
zero_lt_two
{α : Type u_1}
[add_monoid_with_one α]
[partial_order α]
[zero_le_one_class α]
[ne_zero 1]
[covariant_class α α has_add.add has_le.le] :
0 < 2
See zero_lt_two' for a version with the type explicit.
@[simp]
theorem
zero_lt_three
{α : Type u_1}
[add_monoid_with_one α]
[partial_order α]
[zero_le_one_class α]
[ne_zero 1]
[covariant_class α α has_add.add has_le.le] :
0 < 3
See zero_lt_three' for a version with the type explicit.
@[simp]
theorem
zero_lt_four
{α : Type u_1}
[add_monoid_with_one α]
[partial_order α]
[zero_le_one_class α]
[ne_zero 1]
[covariant_class α α has_add.add has_le.le] :
0 < 4
See zero_lt_four' for a version with the type explicit.
theorem
zero_lt_two'
(α : Type u_1)
[add_monoid_with_one α]
[partial_order α]
[zero_le_one_class α]
[ne_zero 1]
[covariant_class α α has_add.add has_le.le] :
0 < 2
See zero_lt_two for a version with the type implicit.
theorem
zero_lt_three'
(α : Type u_1)
[add_monoid_with_one α]
[partial_order α]
[zero_le_one_class α]
[ne_zero 1]
[covariant_class α α has_add.add has_le.le] :
0 < 3
See zero_lt_three for a version with the type implicit.
theorem
zero_lt_four'
(α : Type u_1)
[add_monoid_with_one α]
[partial_order α]
[zero_le_one_class α]
[ne_zero 1]
[covariant_class α α has_add.add has_le.le] :
0 < 4
See zero_lt_four for a version with the type implicit.
@[protected, instance]
def
zero_le_one_class.ne_zero.two
(α : Type u_1)
[add_monoid_with_one α]
[partial_order α]
[zero_le_one_class α]
[ne_zero 1]
[covariant_class α α has_add.add has_le.le] :
ne_zero 2
@[protected, instance]
def
zero_le_one_class.ne_zero.three
(α : Type u_1)
[add_monoid_with_one α]
[partial_order α]
[zero_le_one_class α]
[ne_zero 1]
[covariant_class α α has_add.add has_le.le] :
ne_zero 3
@[protected, instance]
def
zero_le_one_class.ne_zero.four
(α : Type u_1)
[add_monoid_with_one α]
[partial_order α]
[zero_le_one_class α]
[ne_zero 1]
[covariant_class α α has_add.add has_le.le] :
ne_zero 4
theorem
one_lt_two
{α : Type u_1}
[add_monoid_with_one α]
[partial_order α]
[zero_le_one_class α]
[ne_zero 1]
[covariant_class α α has_add.add has_lt.lt] :
1 < 2
theorem
two_pos
{α : Type u_1}
[add_monoid_with_one α]
[partial_order α]
[zero_le_one_class α]
[ne_zero 1]
[covariant_class α α has_add.add has_le.le] :
0 < 2
Alias of zero_lt_two.
theorem
three_pos
{α : Type u_1}
[add_monoid_with_one α]
[partial_order α]
[zero_le_one_class α]
[ne_zero 1]
[covariant_class α α has_add.add has_le.le] :
0 < 3
Alias of zero_lt_three.
theorem
four_pos
{α : Type u_1}
[add_monoid_with_one α]
[partial_order α]
[zero_le_one_class α]
[ne_zero 1]
[covariant_class α α has_add.add has_le.le] :
0 < 4
Alias of zero_lt_four.