Abs

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

Statistics

Metric	Count
Definitions	0
Theorems abs_abs_sub_abs_le_abs_sub, abs_add', abs_add_eq_add_abs_iff, abs_add_three, abs_cases, abs_eq, abs_eq_neg_self, abs_eq_self, abs_le, abs_le_max_abs_abs, abs_max_le_max_abs_abs, abs_min_le_max_abs_abs, abs_nsmul, abs_sub, abs_sub_abs_le_abs_add, abs_sub_abs_le_abs_sub, abs_sub_le, abs_sub_le_iff, abs_sub_le_max_sub, abs_sub_le_of_le_of_le, abs_sub_le_of_nonneg_of_le, abs_sub_lt_iff, abs_sub_lt_of_nonneg_of_lt, abs_sub_nonpos, abs_sub_pos, apply_abs_le_add_of_nonneg, apply_abs_le_add_of_nonneg', apply_abs_le_mul_of_one_le, apply_abs_le_mul_of_one_le', div_le_of_mabs_div_le_left, div_le_of_mabs_div_le_right, div_lt_of_mabs_div_lt_left, div_lt_of_mabs_div_lt_right, eq_of_abs_sub_eq_zero, eq_of_abs_sub_le_all, eq_of_abs_sub_lt_all, eq_of_abs_sub_nonpos, eq_of_mabs_div_eq_one, eq_of_mabs_div_le_all, eq_of_mabs_div_le_one, eq_of_mabs_div_lt_all, inv_le_of_mabs_le, le_abs', le_mabs', le_of_abs_le, le_of_mabs_le, mabs_cases, mabs_div, mabs_div_le, mabs_div_le_iff, mabs_div_le_max_div, mabs_div_le_of_le_of_le, mabs_div_le_of_one_le_of_le, mabs_div_le_one, mabs_div_lt_iff, mabs_div_lt_of_one_le_of_lt, mabs_div_mabs_le_mabs_div, mabs_div_mabs_le_mabs_mul, mabs_div_pos, mabs_eq, mabs_eq_inv_self, mabs_eq_self, mabs_le, mabs_le_max_mabs_mabs, mabs_mabs_div_mabs_le_mabs_div, mabs_max_le_max_mabs_mabs, mabs_min_le_max_mabs_mabs, mabs_mul', mabs_mul_eq_mul_mabs_iff, mabs_mul_three, mabs_pow, max_one_mul_max_inv_one_eq_mabs_self, max_zero_add_max_neg_zero_eq_abs_self, min_abs_abs_le_abs_max, min_abs_abs_le_abs_min, min_mabs_mabs_le_mabs_max, min_mabs_mabs_le_mabs_min, neg_le_of_abs_le, sub_le_of_abs_sub_le_left, sub_le_of_abs_sub_le_right, sub_lt_of_abs_sub_lt_left, sub_lt_of_abs_sub_lt_right	82
Total	82

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_abs_sub_abs_le_abs_sub 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	abs_sub_le_iff abs_sub_abs_le_abs_sub abs_sub_comm
abs_add' 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	neg_add_cancel_left abs_neg abs_add_le IsOrderedAddMonoid.toAddLeftMono
abs_add_eq_add_abs_iff 📖	mathematical	—	abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddGroup AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	le_total add_comm
abs_add_three 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	le_imp_le_of_le_of_le abs_add_le IsOrderedAddMonoid.toAddLeftMono le_refl add_le_add_left covariant_swap_add_of_covariant_add
abs_cases 📖	mathematical	—	abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddGroup Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NegZeroClass.toNeg Preorder.toLT	—	le_or_gt abs_eq_self abs_eq_neg_self le_of_lt
abs_eq 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	abs AddCommGroup.toAddGroup NegZeroClass.toNeg	—	eq_or_eq_neg_of_abs_eq abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono abs_neg
abs_eq_neg_self 📖	mathematical	—	abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddGroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf NegZeroClass.toZero	—	abs_eq_max_neg max_eq_right_iff le_neg_self_iff
abs_eq_self 📖	mathematical	—	abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddGroup Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	abs_eq_max_neg max_eq_left_iff neg_le_self_iff
abs_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	abs_le' neg_le IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add
abs_le_max_abs_abs 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	abs AddCommGroup.toAddGroup SemilatticeSup.toMax Lattice.toSemilatticeSup	—	abs_le' le_sup_iff LE.le.trans le_abs_self neg_le_neg_iff IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add neg_le_abs
abs_max_le_max_abs_abs 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup SemilatticeSup.toMax Lattice.toSemilatticeSup	—	le_total Eq.trans_le max_eq_right le_max_right max_eq_left le_max_left
abs_min_le_max_abs_abs 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	—	le_total Eq.trans_le min_eq_left le_max_left min_eq_right le_max_right
abs_nsmul 📖	mathematical	—	abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddGroup AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	le_total abs_of_nonpos IsOrderedAddMonoid.toAddLeftMono abs_neg neg_nsmul abs_of_nonneg nsmul_nonneg neg_nonneg
abs_sub 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid	—	sub_eq_add_neg abs_neg abs_add_le IsOrderedAddMonoid.toAddLeftMono
abs_sub_abs_le_abs_add 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup abs AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid	—	abs_sub_abs_le_abs_sub sub_neg_eq_add abs_neg
abs_sub_abs_le_abs_sub 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup abs	—	sub_le_iff_le_add covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono sub_add_cancel abs_add_le
abs_sub_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid	—	sub_add_sub_cancel abs_add_le IsOrderedAddMonoid.toAddLeftMono
abs_sub_le_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	abs_le neg_le_sub_iff_le_add IsOrderedAddMonoid.toAddLeftMono sub_le_iff_le_add'
abs_sub_le_max_sub 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid SemilatticeSup.toMax Lattice.toSemilatticeSup	—	le_total abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono sub_nonneg covariant_swap_add_of_covariant_add le_max_of_le_left sub_le_sub_right abs_of_nonpos sub_nonpos neg_sub le_max_of_le_right sub_le_sub_left
abs_sub_le_of_le_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	abs_sub_le_iff sub_le_sub IsOrderedAddMonoid.toAddLeftMono
abs_sub_le_of_nonneg_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	abs_sub_le_iff sub_le_iff_le_add covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono le_add_of_le_of_nonneg
abs_sub_lt_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	abs_lt IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add neg_lt_sub_iff_lt_add' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd sub_lt_iff_lt_add'
abs_sub_lt_of_nonneg_of_lt 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Preorder.toLT	abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	abs_sub_lt_iff sub_lt_iff_lt_add IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono lt_add_of_lt_of_nonneg
abs_sub_nonpos 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	eq_of_abs_sub_nonpos sub_self abs_zero IsOrderedAddMonoid.toAddLeftMono le_refl
abs_sub_pos 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	not_le Iff.not abs_sub_nonpos
apply_abs_le_add_of_nonneg 📖	mathematical	AddZero.toZero AddZeroClass.toAddZero	abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddGroup AddZero.toAdd NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	apply_abs_le_add_of_nonneg'
apply_abs_le_add_of_nonneg' 📖	mathematical	AddZero.toZero AddZeroClass.toAddZero NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddGroup AddZero.toAdd	—	le_add_of_nonneg_left abs_of_nonpos IsOrderedAddMonoid.toAddLeftMono le_add_of_nonneg_right abs_of_nonneg le_total
apply_abs_le_mul_of_one_le 📖	mathematical	MulOne.toOne MulOneClass.toMulOne	abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddGroup MulOne.toMul NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	apply_abs_le_mul_of_one_le'
apply_abs_le_mul_of_one_le' 📖	mathematical	MulOne.toOne MulOneClass.toMulOne NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddGroup MulOne.toMul	—	le_mul_of_one_le_left' abs_of_nonpos IsOrderedAddMonoid.toAddLeftMono le_mul_of_one_le_right' abs_of_nonneg le_total
div_le_of_mabs_div_le_left 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder mabs CommGroup.toGroup DivInvMonoid.toDiv Group.toDivInvMonoid	—	—	div_le_comm IsOrderedMonoid.toMulLeftMono mabs_div_le_iff
div_le_of_mabs_div_le_right 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder mabs CommGroup.toGroup DivInvMonoid.toDiv Group.toDivInvMonoid	—	—	div_le_of_mabs_div_le_left mabs_div_comm
div_lt_of_mabs_div_lt_left 📖	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder mabs CommGroup.toGroup DivInvMonoid.toDiv Group.toDivInvMonoid	—	—	div_lt_comm IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul IsOrderedMonoid.toMulLeftMono mabs_div_lt_iff
div_lt_of_mabs_div_lt_right 📖	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder mabs CommGroup.toGroup DivInvMonoid.toDiv Group.toDivInvMonoid	—	—	div_lt_of_mabs_div_lt_left mabs_div_comm
eq_of_abs_sub_eq_zero 📖	—	abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—	sub_eq_zero abs_eq_zero IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add
eq_of_abs_sub_le_all 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	—	eq_of_abs_sub_nonpos forall_gt_imp_ge_iff_le_of_dense
eq_of_abs_sub_lt_all 📖	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	—	eq_of_abs_sub_nonpos le_of_forall_gt
eq_of_abs_sub_nonpos 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—	eq_of_abs_sub_eq_zero le_antisymm abs_nonneg IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add
eq_of_mabs_div_eq_one 📖	—	mabs DistribLattice.toLattice instDistribLatticeOfLinearOrder CommGroup.toGroup DivInvMonoid.toDiv Group.toDivInvMonoid InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	—	div_eq_one mabs_eq_one IsOrderedMonoid.toMulLeftMono covariant_swap_mul_of_covariant_mul
eq_of_mabs_div_le_all 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder mabs CommGroup.toGroup DivInvMonoid.toDiv Group.toDivInvMonoid	—	—	eq_of_mabs_div_le_one forall_gt_imp_ge_iff_le_of_dense
eq_of_mabs_div_le_one 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder mabs CommGroup.toGroup DivInvMonoid.toDiv Group.toDivInvMonoid InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	—	eq_of_mabs_div_eq_one le_antisymm one_le_mabs IsOrderedMonoid.toMulLeftMono covariant_swap_mul_of_covariant_mul
eq_of_mabs_div_lt_all 📖	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder mabs CommGroup.toGroup DivInvMonoid.toDiv Group.toDivInvMonoid	—	—	eq_of_mabs_div_le_one le_of_forall_gt
inv_le_of_mabs_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder mabs CommGroup.toGroup	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	mabs_le
le_abs' 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	le_abs le_neg IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add
le_mabs' 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder mabs CommGroup.toGroup InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	le_mabs le_inv' IsOrderedMonoid.toMulLeftMono covariant_swap_mul_of_covariant_mul
le_of_abs_le 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup	—	—	abs_le
le_of_mabs_le 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder mabs CommGroup.toGroup	—	—	mabs_le
mabs_cases 📖	mathematical	—	mabs DistribLattice.toLattice instDistribLatticeOfLinearOrder CommGroup.toGroup Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid InvOneClass.toInv Preorder.toLT	—	le_or_gt
mabs_div 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder mabs CommGroup.toGroup DivInvMonoid.toDiv Group.toDivInvMonoid MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid	—	div_eq_mul_inv mabs_inv mabs_mul_le IsOrderedMonoid.toMulLeftMono
mabs_div_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder mabs CommGroup.toGroup DivInvMonoid.toDiv Group.toDivInvMonoid MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid	—	div_mul_div_cancel mabs_mul_le IsOrderedMonoid.toMulLeftMono
mabs_div_le_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder mabs CommGroup.toGroup DivInvMonoid.toDiv Group.toDivInvMonoid	—	mabs_le inv_le_div_iff_le_mul IsOrderedMonoid.toMulLeftMono div_le_iff_le_mul'
mabs_div_le_max_div 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	mabs CommGroup.toGroup DivInvMonoid.toDiv Group.toDivInvMonoid SemilatticeSup.toMax Lattice.toSemilatticeSup	—	le_total mabs_of_one_le IsOrderedMonoid.toMulLeftMono one_le_div' covariant_swap_mul_of_covariant_mul le_max_of_le_left div_le_div_right' mabs_of_le_one div_le_one' inv_div le_max_of_le_right div_le_div_left'
mabs_div_le_of_le_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	mabs CommGroup.toGroup DivInvMonoid.toDiv Group.toDivInvMonoid	—	mabs_div_le_iff div_le_div'' IsOrderedMonoid.toMulLeftMono
mabs_div_le_of_one_le_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	mabs CommGroup.toGroup DivInvMonoid.toDiv Group.toDivInvMonoid	—	mabs_div_le_iff div_le_iff_le_mul covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono le_mul_of_le_of_one_le
mabs_div_le_one 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder mabs CommGroup.toGroup DivInvMonoid.toDiv Group.toDivInvMonoid InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	eq_of_mabs_div_le_one div_self' mabs_one IsOrderedMonoid.toMulLeftMono le_refl
mabs_div_lt_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder mabs CommGroup.toGroup DivInvMonoid.toDiv Group.toDivInvMonoid	—	mabs_lt IsOrderedMonoid.toMulLeftMono covariant_swap_mul_of_covariant_mul inv_lt_div_iff_lt_mul' IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul div_lt_iff_lt_mul'
mabs_div_lt_of_one_le_of_lt 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid Preorder.toLT	mabs CommGroup.toGroup DivInvMonoid.toDiv Group.toDivInvMonoid	—	mabs_div_lt_iff div_lt_iff_lt_mul IsRightCancelMul.mulRightStrictMono_of_mulRightMono RightCancelSemigroup.toIsRightCancelMul covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono lt_mul_of_lt_of_one_le
mabs_div_mabs_le_mabs_div 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DivInvMonoid.toDiv Group.toDivInvMonoid CommGroup.toGroup mabs	—	div_le_iff_le_mul covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono div_mul_cancel mabs_mul_le
mabs_div_mabs_le_mabs_mul 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DivInvMonoid.toDiv Group.toDivInvMonoid CommGroup.toGroup mabs MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid	—	mabs_div_mabs_le_mabs_div div_inv_eq_mul mabs_inv
mabs_div_pos 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid mabs CommGroup.toGroup DivInvMonoid.toDiv Group.toDivInvMonoid	—	not_le Iff.not mabs_div_le_one
mabs_eq 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	mabs CommGroup.toGroup InvOneClass.toInv	—	eq_or_eq_inv_of_mabs_eq mabs_of_one_le IsOrderedMonoid.toMulLeftMono mabs_inv
mabs_eq_inv_self 📖	mathematical	—	mabs DistribLattice.toLattice instDistribLatticeOfLinearOrder CommGroup.toGroup InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf InvOneClass.toOne	—	mabs_eq_max_inv max_eq_right_iff le_inv_self_iff
mabs_eq_self 📖	mathematical	—	mabs DistribLattice.toLattice instDistribLatticeOfLinearOrder CommGroup.toGroup Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	mabs_eq_max_inv max_eq_left_iff inv_le_self_iff
mabs_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder mabs CommGroup.toGroup InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	mabs_le' inv_le' IsOrderedMonoid.toMulLeftMono covariant_swap_mul_of_covariant_mul
mabs_le_max_mabs_mabs 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	mabs CommGroup.toGroup SemilatticeSup.toMax Lattice.toSemilatticeSup	—	mabs_le' LE.le.trans le_mabs_self inv_le_inv_iff IsOrderedMonoid.toMulLeftMono covariant_swap_mul_of_covariant_mul inv_le_mabs
mabs_mabs_div_mabs_le_mabs_div 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder mabs CommGroup.toGroup DivInvMonoid.toDiv Group.toDivInvMonoid	—	mabs_div_le_iff mabs_div_mabs_le_mabs_div mabs_div_comm
mabs_max_le_max_mabs_mabs 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder mabs CommGroup.toGroup SemilatticeSup.toMax Lattice.toSemilatticeSup	—	le_total Eq.trans_le max_eq_right le_max_right max_eq_left le_max_left
mabs_min_le_max_mabs_mabs 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder mabs CommGroup.toGroup SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	—	le_total Eq.trans_le min_eq_left le_max_left min_eq_right le_max_right
mabs_mul' 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder mabs CommGroup.toGroup MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	inv_mul_cancel_left mabs_inv mabs_mul_le IsOrderedMonoid.toMulLeftMono
mabs_mul_eq_mul_mabs_iff 📖	mathematical	—	mabs DistribLattice.toLattice instDistribLatticeOfLinearOrder CommGroup.toGroup MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	le_total mul_comm
mabs_mul_three 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder mabs CommGroup.toGroup MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	le_imp_le_of_le_of_le mabs_mul_le IsOrderedMonoid.toMulLeftMono le_refl mul_le_mul_left covariant_swap_mul_of_covariant_mul
mabs_pow 📖	mathematical	—	mabs DistribLattice.toLattice instDistribLatticeOfLinearOrder CommGroup.toGroup Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid	—	le_total mabs_of_le_one IsOrderedMonoid.toMulLeftMono mabs_inv inv_pow mabs_of_one_le one_le_pow_of_one_le' one_le_inv'
max_one_mul_max_inv_one_eq_mabs_self 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid InvOneClass.toInv mabs	—	le_total sup_of_le_left sup_of_le_right IsOrderedMonoid.toMulLeftMono mul_one one_mul
max_zero_add_max_neg_zero_eq_abs_self 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NegZeroClass.toNeg abs	—	le_total sup_of_le_left sup_of_le_right Left.neg_nonpos_iff IsOrderedAddMonoid.toAddLeftMono add_zero abs_eq_self Left.nonneg_neg_iff zero_add abs_eq_neg_self
min_abs_abs_le_abs_max 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin abs AddCommGroup.toAddGroup SemilatticeSup.toMax Lattice.toSemilatticeSup	—	le_total LE.le.trans_eq min_le_right max_eq_right min_le_left max_eq_left
min_abs_abs_le_abs_min 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin abs AddCommGroup.toAddGroup	—	le_total LE.le.trans_eq min_le_left min_eq_left min_le_right min_eq_right
min_mabs_mabs_le_mabs_max 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin mabs CommGroup.toGroup SemilatticeSup.toMax Lattice.toSemilatticeSup	—	le_total LE.le.trans_eq min_le_right max_eq_right min_le_left max_eq_left
min_mabs_mabs_le_mabs_min 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin mabs CommGroup.toGroup	—	le_total LE.le.trans_eq min_le_left min_eq_left min_le_right min_eq_right
neg_le_of_abs_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	abs_le
sub_le_of_abs_sub_le_left 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	—	sub_le_comm IsOrderedAddMonoid.toAddLeftMono abs_sub_le_iff
sub_le_of_abs_sub_le_right 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	—	sub_le_of_abs_sub_le_left abs_sub_comm
sub_lt_of_abs_sub_lt_left 📖	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	—	sub_lt_comm IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono abs_sub_lt_iff
sub_lt_of_abs_sub_lt_right 📖	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	—	sub_lt_of_abs_sub_lt_left abs_sub_comm

---

← Back to Index