MinMax

📁 Source: Mathlib/Algebra/Order/Group/MinMax.lean

Statistics

Metric	Count
Definitions	0
Theorems abs_max_sub_max_le_abs, abs_max_sub_max_le_max, abs_min_sub_min_le_max, max_div_div_left', max_div_div_right', max_inv_inv', max_inv_one, max_neg_neg, max_neg_zero, max_one_div_max_inv_one_eq_self, max_sub_max_le_max, max_sub_sub_left, max_sub_sub_right, max_zero_sub_eq_self, max_zero_sub_max_neg_zero_eq_self, min_div_div_left', min_div_div_right', min_inv_inv', min_neg_neg, min_sub_sub_left, min_sub_sub_right	21
Total	21

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_max_sub_max_le_abs 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid SemilatticeSup.toMax Lattice.toSemilatticeSup	—	sub_self abs_zero IsOrderedAddMonoid.toAddLeftMono max_eq_left abs_nonneg covariant_swap_add_of_covariant_add abs_max_sub_max_le_max
abs_max_sub_max_le_max 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid SemilatticeSup.toMax Lattice.toSemilatticeSup	—	abs_sub_le_iff LE.le.trans max_sub_max_le_max max_le_max le_abs_self abs_sub_comm
abs_min_sub_min_le_max 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	—	max_neg_neg neg_sub_neg abs_sub_comm abs_max_sub_max_le_max
max_div_div_left' 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder DivInvMonoid.toDiv Group.toDivInvMonoid CommGroup.toGroup SemilatticeInf.toMin Lattice.toSemilatticeInf	—	div_eq_mul_inv max_mul_mul_left IsOrderedMonoid.toMulLeftMono max_inv_inv'
max_div_div_right' 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder DivInvMonoid.toDiv Group.toDivInvMonoid CommGroup.toGroup	—	div_eq_mul_inv max_mul_mul_right covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono
max_inv_inv' 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid SemilatticeInf.toMin Lattice.toSemilatticeInf	—	Monotone.map_min inv_le_inv_iff IsOrderedMonoid.toMulLeftMono covariant_swap_mul_of_covariant_mul
max_inv_one 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid InvOneClass.toOne MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	eq_inv_mul_iff_mul_eq eq_div_iff_mul_eq' max_one_div_max_inv_one_eq_self
max_neg_neg 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SemilatticeInf.toMin Lattice.toSemilatticeInf	—	Monotone.map_min neg_le_neg_iff IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add
max_neg_zero 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid NegZeroClass.toZero AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	eq_neg_add_iff_add_eq eq_sub_iff_add_eq max_zero_sub_max_neg_zero_eq_self
max_one_div_max_inv_one_eq_self 📖	mathematical	—	DivInvMonoid.toDiv Group.toDivInvMonoid SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid InvOneClass.toInv	—	le_total sup_of_le_right sup_of_le_left div_inv_eq_mul one_mul div_one
max_sub_max_le_max 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
max_sub_sub_left 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SemilatticeInf.toMin Lattice.toSemilatticeInf	—	sub_eq_add_neg max_add_add_left IsOrderedAddMonoid.toAddLeftMono max_neg_neg
max_sub_sub_right 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	sub_eq_add_neg max_add_add_right covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono
max_zero_sub_eq_self 📖	mathematical	—	SubNegMonoid.toSub AddGroup.toSubNegMonoid SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid NegZeroClass.toNeg	—	max_zero_sub_max_neg_zero_eq_self
max_zero_sub_max_neg_zero_eq_self 📖	mathematical	—	SubNegMonoid.toSub AddGroup.toSubNegMonoid SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid NegZeroClass.toNeg	—	le_total sup_of_le_right sup_of_le_left Left.nonneg_neg_iff sub_neg_eq_add zero_add Left.neg_nonpos_iff sub_zero
min_div_div_left' 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DivInvMonoid.toDiv Group.toDivInvMonoid CommGroup.toGroup SemilatticeSup.toMax Lattice.toSemilatticeSup	—	div_eq_mul_inv min_mul_mul_left IsOrderedMonoid.toMulLeftMono min_inv_inv'
min_div_div_right' 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DivInvMonoid.toDiv Group.toDivInvMonoid CommGroup.toGroup	—	div_eq_mul_inv min_mul_mul_right covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono
min_inv_inv' 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid SemilatticeSup.toMax Lattice.toSemilatticeSup	—	Monotone.map_max inv_le_inv_iff IsOrderedMonoid.toMulLeftMono covariant_swap_mul_of_covariant_mul
min_neg_neg 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SemilatticeSup.toMax Lattice.toSemilatticeSup	—	Monotone.map_max neg_le_neg_iff IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add
min_sub_sub_left 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SemilatticeSup.toMax Lattice.toSemilatticeSup	—	sub_eq_add_neg min_add_add_left IsOrderedAddMonoid.toAddLeftMono min_neg_neg
min_sub_sub_right 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	sub_eq_add_neg min_add_add_right covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono

---

← Back to Index