mathlib3 documentation

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.

theorem min_neg_neg {α : Type u_1} [linear_ordered_add_comm_group α] (a b : α) :
theorem max_neg_neg {α : Type u_1} [linear_ordered_add_comm_group α] (a b : α) :
theorem min_div_div_right' {α : Type u_1} [linear_ordered_comm_group α] (a b c : α) :
theorem min_sub_sub_right {α : Type u_1} [linear_ordered_add_comm_group α] (a b c : α) :
theorem max_div_div_right' {α : Type u_1} [linear_ordered_comm_group α] (a b c : α) :
theorem max_sub_sub_right {α : Type u_1} [linear_ordered_add_comm_group α] (a b c : α) :
theorem min_div_div_left' {α : Type u_1} [linear_ordered_comm_group α] (a b c : α) :
theorem min_sub_sub_left {α : Type u_1} [linear_ordered_add_comm_group α] (a b c : α) :
theorem max_div_div_left' {α : Type u_1} [linear_ordered_comm_group α] (a b c : α) :
theorem max_sub_sub_left {α : Type u_1} [linear_ordered_add_comm_group α] (a b c : α) :
theorem max_sub_max_le_max {α : Type u_1} [linear_ordered_add_comm_group α] (a b c d : α) :