# mathlib3documentation

algebra.order.group.min_max

# min and max in linearly ordered groups. #

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

@[simp]
theorem max_zero_sub_max_neg_zero_eq_self {α : Type u_1} [add_group α] [linear_order α] (a : α) :
- 0 = a
@[simp]
theorem max_one_div_max_inv_one_eq_self {α : Type u_1} [group α] [linear_order α] (a : α) :
= a
theorem max_zero_sub_eq_self {α : Type u_1} [add_group α] [linear_order α] (a : α) :
- 0 = a

Alias of max_zero_sub_max_neg_zero_eq_self.

theorem min_neg_neg {α : Type u_1} (a b : α) :
(-b) =
theorem min_inv_inv' {α : Type u_1} (a b : α) :
= b)⁻¹
theorem max_inv_inv' {α : Type u_1} (a b : α) :
= b)⁻¹
theorem max_neg_neg {α : Type u_1} (a b : α) :
(-b) =
theorem min_div_div_right' {α : Type u_1} (a b c : α) :
linear_order.min (a / c) (b / c) = / c
theorem min_sub_sub_right {α : Type u_1} (a b c : α) :
linear_order.min (a - c) (b - c) = - c
theorem max_div_div_right' {α : Type u_1} (a b c : α) :
linear_order.max (a / c) (b / c) = / c
theorem max_sub_sub_right {α : Type u_1} (a b c : α) :
linear_order.max (a - c) (b - c) = - c
theorem min_div_div_left' {α : Type u_1} (a b c : α) :
linear_order.min (a / b) (a / c) = a /
theorem min_sub_sub_left {α : Type u_1} (a b c : α) :
linear_order.min (a - b) (a - c) = a -
theorem max_div_div_left' {α : Type u_1} (a b c : α) :
linear_order.max (a / b) (a / c) = a /
theorem max_sub_sub_left {α : Type u_1} (a b c : α) :
linear_order.max (a - b) (a - c) = a -
theorem max_sub_max_le_max {α : Type u_1} (a b c d : α) :
linear_order.max (a - c) (b - d)
theorem abs_max_sub_max_le_max {α : Type u_1} (a b c d : α) :
|| |b - d|
theorem abs_min_sub_min_le_max {α : Type u_1} (a b c d : α) :
|| |b - d|
theorem abs_max_sub_max_le_abs {α : Type u_1} (a b c : α) :
|| |a - b|