min
and max
in linearly ordered groups. #
@[simp]
theorem
max_zero_sub_max_neg_zero_eq_self
{α : Type u_1}
[inst : AddGroup α]
[inst : LinearOrder α]
[inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
(a : α)
:
@[simp]
theorem
max_one_div_max_inv_one_eq_self
{α : Type u_1}
[inst : Group α]
[inst : LinearOrder α]
[inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
(a : α)
:
theorem
max_zero_sub_eq_self
{α : Type u_1}
[inst : AddGroup α]
[inst : LinearOrder α]
[inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
(a : α)
:
Alias of max_zero_sub_max_neg_zero_eq_self
.