min
and max
in linearly ordered groups. #
@[simp]
theorem
max_zero_sub_max_neg_zero_eq_self
{α : Type u_1}
[AddGroup α]
[LinearOrder α]
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
(a : α)
:
@[simp]
theorem
max_one_div_max_inv_one_eq_self
{α : Type u_1}
[Group α]
[LinearOrder α]
[CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2]
(a : α)
:
theorem
max_zero_sub_eq_self
{α : Type u_1}
[AddGroup α]
[LinearOrder α]
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
(a : α)
:
Alias of max_zero_sub_max_neg_zero_eq_self
.
theorem
max_neg_zero
{α : Type u_1}
[AddGroup α]
[LinearOrder α]
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
(a : α)
:
theorem
max_inv_one
{α : Type u_1}
[Group α]
[LinearOrder α]
[CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2]
(a : α)
:
theorem
abs_max_sub_max_le_abs
{α : Type u_1}
[LinearOrderedAddCommGroup α]
(a : α)
(b : α)
(c : α)
: