Basic

📁 Source: Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems const_mul_of_nonpos, mul, mul_const_of_nonpos, mul_monotone, const_mul_of_nonpos, mul_antitone, mul_const_of_nonpos, const_mul_of_neg, mul_const_of_neg, const_mul_of_neg, mul_const_of_neg, inv_neg, inv_pos, add_le_mul, add_le_mul', add_le_mul_of_left_le_right, add_le_mul_of_right_le_left, add_le_mul_two_add, add_one_le_two_mul, antitone_mul_left, antitone_mul_right, cmp_mul_neg_left, cmp_mul_neg_right, cmp_mul_pos_left, cmp_mul_pos_right, eq_zero_of_mul_self_add_mul_self_eq_zero, four_mul_le_pow_two_add, four_mul_le_sq_add, le_mul_of_le_one_left, le_mul_of_le_one_right, le_of_mul_le_of_one_le, lt_mul_of_lt_one_left, lt_mul_of_lt_one_right, lt_of_mul_lt_mul_of_nonpos_left, lt_of_mul_lt_mul_of_nonpos_right, lt_two_mul_self, max_mul_mul_le_max_mul_max, max_mul_of_nonneg, min_mul_of_nonneg, mul_add_mul_le_mul_add_mul, mul_add_mul_le_mul_add_mul', mul_add_mul_lt_mul_add_mul, mul_add_mul_lt_mul_add_mul', mul_le_mul_left_of_neg, mul_le_mul_of_nonneg_of_nonpos, mul_le_mul_of_nonneg_of_nonpos', mul_le_mul_of_nonpos_left, mul_le_mul_of_nonpos_of_nonneg, mul_le_mul_of_nonpos_of_nonneg', mul_le_mul_of_nonpos_of_nonpos, mul_le_mul_of_nonpos_of_nonpos', mul_le_mul_of_nonpos_right, mul_le_mul_right_of_neg, mul_le_of_one_le_left, mul_le_of_one_le_right, mul_lt_mul_left_of_neg, mul_lt_mul_of_neg_left, mul_lt_mul_of_neg_right, mul_lt_mul_right_of_neg, mul_lt_of_one_lt_left, mul_lt_of_one_lt_right, mul_max_of_nonneg, mul_min_of_nonneg, mul_neg_iff, mul_nonneg_iff, mul_nonneg_iff_left_nonneg_of_pos, mul_nonneg_iff_neg_imp_nonpos, mul_nonneg_iff_of_pos_left, mul_nonneg_iff_of_pos_right, mul_nonneg_iff_pos_imp_nonneg, mul_nonneg_iff_right_nonneg_of_pos, mul_nonneg_of_nonpos_of_nonpos, mul_nonneg_of_three, mul_nonpos_iff, mul_nonpos_iff_neg_imp_nonneg, mul_nonpos_iff_pos_imp_nonpos, mul_pos_iff, mul_pos_of_neg_of_neg, mul_self_add_mul_self_eq_zero, mul_self_inj, mul_self_le_mul_self_iff, mul_self_le_mul_self_of_le_of_neg_le, mul_self_lt_mul_self_iff, mul_self_nonneg, mul_self_pos, neg_iff_pos_of_mul_neg, neg_one_lt_zero, nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nonneg, nonneg_le_nonneg_of_sq_le_sq, nonneg_of_mul_nonneg_left, nonneg_of_mul_nonneg_right, nonneg_of_mul_nonpos_left, nonneg_of_mul_nonpos_right, nonpos_of_mul_nonneg_left, nonpos_of_mul_nonneg_right, nonpos_of_mul_nonpos_left, nonpos_of_mul_nonpos_right, pos_iff_neg_of_mul_neg, pos_of_left_mul_lt_le, pos_of_mul_neg_left, pos_of_mul_neg_right, pos_of_right_mul_lt_le, pow_two_nonneg, sign_cases_of_C_mul_pow_nonneg, sq_nonneg, sq_nonpos_iff, strictAnti_mul_left, strictAnti_mul_right, sub_mul_sub_neg_iff, sub_mul_sub_nonneg_iff, sub_mul_sub_nonpos_iff, sub_mul_sub_pos_iff, sub_one_lt, two_mul_le_add_of_sq_eq_mul, two_mul_le_add_pow_two, two_mul_le_add_sq	116
Total	116

Antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
const_mul_of_nonpos 📖	mathematical	Antitone Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Monotone Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	comp antitone_mul_left
mul 📖	mathematical	Antitone Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Monotone Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_le_mul_of_nonpos_of_nonpos
mul_const_of_nonpos 📖	mathematical	Antitone Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Monotone Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	comp antitone_mul_right
mul_monotone 📖	mathematical	Antitone Monotone Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_le_mul_of_nonpos_of_nonneg

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
const_mul_of_nonpos 📖	mathematical	Monotone Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Antitone Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	Antitone.comp_monotone antitone_mul_left
mul_antitone 📖	mathematical	Monotone Antitone Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_le_mul_of_nonneg_of_nonpos
mul_const_of_nonpos 📖	mathematical	Monotone Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Antitone Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	Antitone.comp_monotone antitone_mul_right

StrictAnti

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
const_mul_of_neg 📖	mathematical	StrictAnti PartialOrder.toPreorder Preorder.toLT MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	StrictMono Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	comp strictAnti_mul_left
mul_const_of_neg 📖	mathematical	StrictAnti PartialOrder.toPreorder Preorder.toLT MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	StrictMono Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	comp strictAnti_mul_right

StrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
const_mul_of_neg 📖	mathematical	StrictMono PartialOrder.toPreorder Preorder.toLT MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	StrictAnti Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	StrictAnti.comp_strictMono strictAnti_mul_left
mul_const_of_neg 📖	mathematical	StrictMono PartialOrder.toPreorder Preorder.toLT MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	StrictAnti Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	StrictAnti.comp_strictMono strictAnti_mul_right

Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inv_neg 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Units instInv MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	neg_of_mul_pos_right zero_lt_one mul_inv LT.lt.le
inv_pos 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Units instInv	—	mul_pos_iff_of_pos_left PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE zero_lt_one mul_inv

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_le_mul 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Nat.instAtLeastTwoHAddOfNat	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toMul	—	Nat.instAtLeastTwoHAddOfNat add_le_mul_of_left_le_right add_le_mul_of_right_le_left le_of_not_ge
add_le_mul' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Nat.instAtLeastTwoHAddOfNat	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toMul	—	Nat.instAtLeastTwoHAddOfNat LE.le.trans le_of_eq add_comm add_le_mul
add_le_mul_of_left_le_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Nat.instAtLeastTwoHAddOfNat	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toMul	—	Nat.instAtLeastTwoHAddOfNat zero_lt_two add_le_add_left covariant_swap_add_of_covariant_add two_mul mul_le_mul_iff_left₀ MulPosStrictMono.toMulPosMono MulPosStrictMono.toMulPosReflectLE
add_le_mul_of_right_le_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Nat.instAtLeastTwoHAddOfNat	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toMul	—	Nat.instAtLeastTwoHAddOfNat zero_lt_two add_le_add_right mul_two mul_le_mul_iff_right₀ PosMulStrictMono.toPosMulMono PosMulStrictMono.toPosMulReflectLE
add_le_mul_two_add 📖	mathematical	Preorder.toLE instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Nat.instAtLeastTwoHAddOfNat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Distrib.toMul	—	Nat.instAtLeastTwoHAddOfNat add_le_add_right add_le_add covariant_swap_add_of_covariant_add le_mul_of_one_le_left LE.le.trans one_le_two mul_add Distrib.leftDistribClass mul_two add_assoc le_refl
add_one_le_two_mul 📖	mathematical	AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toMul instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat add_le_add_right two_mul
antitone_mul_left 📖	mathematical	Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Antitone Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_le_mul_of_nonpos_left
antitone_mul_right 📖	mathematical	Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Antitone Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_le_mul_of_nonpos_right
cmp_mul_neg_left 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	cmp LinearOrder.toDecidableLT Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	StrictAnti.cmp_map_eq strictAnti_mul_left
cmp_mul_neg_right 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	cmp LinearOrder.toDecidableLT Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	StrictAnti.cmp_map_eq strictAnti_mul_right
cmp_mul_pos_left 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	cmp LinearOrder.toDecidableLT Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	StrictMono.cmp_map_eq strictMono_mul_left_of_pos
cmp_mul_pos_right 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	cmp LinearOrder.toDecidableLT Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	StrictMono.cmp_map_eq strictMono_mul_right_of_pos
eq_zero_of_mul_self_add_mul_self_eq_zero 📖	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—	mul_self_add_mul_self_eq_zero
four_mul_le_pow_two_add 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.instAtLeastTwoHAddOfNat Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd	—	four_mul_le_sq_add
four_mul_le_sq_add 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.instAtLeastTwoHAddOfNat Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toAdd	—	Nat.instAtLeastTwoHAddOfNat mul_assoc two_add_two_eq_four add_mul Distrib.rightDistribClass add_le_add_left covariant_swap_add_of_covariant_add two_mul_le_add_sq add_right_comm add_sq
le_mul_of_le_one_left 📖	mathematical	Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	one_mul mul_le_mul_of_nonpos_right
le_mul_of_le_one_right 📖	mathematical	Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_one mul_le_mul_of_nonpos_left
le_of_mul_le_of_one_le 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—	le_of_mul_le_mul_right MulPosStrictMono.toMulPosReflectLE LE.le.trans le_mul_of_one_le_right LT.lt.trans_le zero_lt_one
lt_mul_of_lt_one_left 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	one_mul mul_lt_mul_of_neg_right
lt_mul_of_lt_one_right 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_one mul_lt_mul_of_neg_left
lt_of_mul_lt_mul_of_nonpos_left 📖	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—	Antitone.reflect_lt antitone_mul_left
lt_of_mul_lt_mul_of_nonpos_right 📖	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—	Antitone.reflect_lt antitone_mul_right
lt_two_mul_self 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.instAtLeastTwoHAddOfNat	—	lt_mul_of_one_lt_left Nat.instAtLeastTwoHAddOfNat one_lt_two
max_mul_mul_le_max_mul_max 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	SemilatticeSup.toMax Lattice.toSemilatticeSup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_le_mul le_max_right LE.le.trans le_max_left le_trans max_le mul_comm max_comm
max_mul_of_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SemilatticeSup.toMax Lattice.toSemilatticeSup	—	Monotone.map_max monotone_mul_right_of_nonneg
min_mul_of_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SemilatticeInf.toMin	—	Monotone.map_min monotone_mul_right_of_nonneg
mul_add_mul_le_mul_add_mul 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul	—	exists_nonneg_add_of_le mul_add Distrib.leftDistribClass add_right_comm add_assoc add_le_add_right mul_le_mul_of_nonneg_right
mul_add_mul_le_mul_add_mul' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul	—	add_comm mul_add_mul_le_mul_add_mul
mul_add_mul_lt_mul_add_mul 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul	—	exists_pos_add_of_lt' mul_add Distrib.leftDistribClass add_right_comm add_assoc add_lt_add_right mul_lt_mul_of_pos_right
mul_add_mul_lt_mul_add_mul' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul	—	add_comm mul_add_mul_lt_mul_add_mul
mul_le_mul_left_of_neg 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Preorder.toLE Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	StrictAnti.le_iff_ge strictAnti_mul_left covariant_lt_of_contravariant_le contravariant_lt_of_covariant_le
mul_le_mul_of_nonneg_of_nonpos 📖	mathematical	Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	LE.le.trans mul_le_mul_of_nonpos_right mul_le_mul_of_nonneg_left
mul_le_mul_of_nonneg_of_nonpos' 📖	mathematical	Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	LE.le.trans mul_le_mul_of_nonneg_left mul_le_mul_of_nonpos_right
mul_le_mul_of_nonpos_left 📖	mathematical	Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	ExistsAddOfLE.exists_add_of_le le_of_add_le_add_right add_left_comm add_mul Distrib.rightDistribClass MulZeroClass.zero_mul add_zero mul_le_mul_of_nonneg_left Eq.trans_le add_le_of_nonpos_left add_assoc zero_add
mul_le_mul_of_nonpos_of_nonneg 📖	mathematical	Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	LE.le.trans mul_le_mul_of_nonneg_right mul_le_mul_of_nonpos_left
mul_le_mul_of_nonpos_of_nonneg' 📖	mathematical	Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	LE.le.trans mul_le_mul_of_nonneg_left mul_le_mul_of_nonpos_right
mul_le_mul_of_nonpos_of_nonpos 📖	mathematical	Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	LE.le.trans mul_le_mul_of_nonpos_right mul_le_mul_of_nonpos_left
mul_le_mul_of_nonpos_of_nonpos' 📖	mathematical	Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	LE.le.trans mul_le_mul_of_nonpos_left mul_le_mul_of_nonpos_right
mul_le_mul_of_nonpos_right 📖	mathematical	Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	ExistsAddOfLE.exists_add_of_le le_of_add_le_add_right add_left_comm mul_add Distrib.leftDistribClass MulZeroClass.mul_zero add_zero mul_le_mul_of_nonneg_right Eq.trans_le add_le_of_nonpos_left add_assoc zero_add
mul_le_mul_right_of_neg 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Preorder.toLE Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	StrictAnti.le_iff_ge strictAnti_mul_right covariant_lt_of_contravariant_le contravariant_lt_of_covariant_le
mul_le_of_one_le_left 📖	mathematical	Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	one_mul mul_le_mul_of_nonpos_right
mul_le_of_one_le_right 📖	mathematical	Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_one mul_le_mul_of_nonpos_left
mul_lt_mul_left_of_neg 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	StrictAnti.lt_iff_gt strictAnti_mul_left
mul_lt_mul_of_neg_left 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	ExistsAddOfLE.exists_add_of_le LT.lt.le add_lt_add_iff_right add_left_comm add_mul Distrib.rightDistribClass MulZeroClass.zero_mul add_zero mul_lt_mul_of_pos_left Eq.trans_lt add_lt_of_neg_left add_assoc zero_add
mul_lt_mul_of_neg_right 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	ExistsAddOfLE.exists_add_of_le LT.lt.le add_lt_add_iff_right add_left_comm mul_add Distrib.leftDistribClass MulZeroClass.mul_zero add_zero mul_lt_mul_of_pos_right Eq.trans_lt add_lt_of_neg_left add_assoc zero_add
mul_lt_mul_right_of_neg 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	StrictAnti.lt_iff_gt strictAnti_mul_right
mul_lt_of_one_lt_left 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	one_mul mul_lt_mul_of_neg_right
mul_lt_of_one_lt_right 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_one mul_lt_mul_of_neg_left
mul_max_of_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SemilatticeSup.toMax Lattice.toSemilatticeSup	—	Monotone.map_max monotone_mul_left_of_nonneg
mul_min_of_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SemilatticeInf.toMin	—	Monotone.map_min monotone_mul_left_of_nonneg
mul_neg_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	neg_pos neg_mul_eq_mul_neg mul_pos_iff AddGroup.existsAddOfLE neg_lt_zero
mul_nonneg_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nonneg mul_nonneg PosMulStrictMono.toPosMulMono mul_nonneg_of_nonpos_of_nonpos MulPosStrictMono.toMulPosMono covariant_swap_add_of_covariant_add contravariant_swap_add_of_contravariant_add
mul_nonneg_iff_left_nonneg_of_pos 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Preorder.toLE Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	nonneg_of_mul_nonneg_left mul_nonneg PosMulStrictMono.toPosMulMono LT.lt.le
mul_nonneg_iff_neg_imp_nonpos 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	neg_mul_neg mul_nonneg_iff_pos_imp_nonneg AddGroup.existsAddOfLE IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd
mul_nonneg_iff_of_pos_left 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Preorder.toLE Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	MulZeroClass.mul_zero mul_le_mul_iff_right₀ PosMulStrictMono.toPosMulMono PosMulStrictMono.toPosMulReflectLE
mul_nonneg_iff_of_pos_right 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Preorder.toLE Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	MulZeroClass.zero_mul mul_le_mul_iff_left₀ MulPosStrictMono.toMulPosMono MulPosStrictMono.toMulPosReflectLE
mul_nonneg_iff_pos_imp_nonneg 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_nonneg_iff le_total
mul_nonneg_iff_right_nonneg_of_pos 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Preorder.toLE Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	nonneg_of_mul_nonneg_right mul_nonneg PosMulStrictMono.toPosMulMono LT.lt.le
mul_nonneg_of_nonpos_of_nonpos 📖	mathematical	Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	MulZeroClass.zero_mul mul_le_mul_of_nonpos_right
mul_nonneg_of_three 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_nonneg_iff le_total
mul_nonpos_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	neg_nonneg neg_mul_eq_mul_neg mul_nonneg_iff AddGroup.existsAddOfLE neg_nonpos
mul_nonpos_iff_neg_imp_nonneg 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	neg_nonneg neg_mul mul_nonneg_iff_pos_imp_nonneg AddGroup.existsAddOfLE IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd
mul_nonpos_iff_pos_imp_nonpos 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	neg_nonneg mul_neg mul_nonneg_iff_pos_imp_nonneg AddGroup.existsAddOfLE IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd
mul_pos_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	pos_and_pos_or_neg_and_neg_of_mul_pos PosMulStrictMono.toPosMulMono MulPosStrictMono.toMulPosMono mul_pos mul_pos_of_neg_of_neg covariant_swap_add_of_covariant_add contravariant_swap_add_of_contravariant_add
mul_pos_of_neg_of_neg 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	MulZeroClass.zero_mul mul_lt_mul_of_neg_right
mul_self_add_mul_self_eq_zero 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	add_eq_zero_iff_of_nonneg covariant_swap_add_of_covariant_add mul_self_nonneg mul_self_eq_zero
mul_self_inj 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	StrictMonoOn.eq_iff_eq strictMonoOn_mul_self
mul_self_le_mul_self_iff 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_self_le_mul_self PosMulStrictMono.toPosMulMono nonneg_le_nonneg_of_sq_le_sq
mul_self_le_mul_self_of_le_of_neg_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	le_total mul_self_le_mul_self Eq.trans_le neg_mul_neg mul_le_mul neg_nonneg LE.le.trans
mul_self_lt_mul_self_iff 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Preorder.toLT Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	StrictMonoOn.lt_iff_lt strictMonoOn_mul_self
mul_self_nonneg 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	sq sq_nonneg
mul_self_pos 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	LT.lt.false MulZeroClass.mul_zero Ne.lt_or_gt mul_pos_of_neg_of_neg covariant_swap_add_of_covariant_add contravariant_swap_add_of_contravariant_add mul_pos
neg_iff_pos_of_mul_neg 📖	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—	pos_of_mul_neg_right le_of_lt neg_of_mul_neg_left
neg_one_lt_zero 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	neg_lt_zero zero_lt_one
nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nonneg 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—	not_lt_of_ge lt_trichotomy mul_neg_of_pos_of_neg LT.lt.le LT.lt.asymm le_rfl mul_neg_of_neg_of_pos
nonneg_le_nonneg_of_sq_le_sq 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—	le_of_not_gt LT.lt.not_ge mul_self_lt_mul_self
nonneg_of_mul_nonneg_left 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Preorder.toLT	—	—	le_of_not_gt LT.lt.not_ge mul_neg_of_neg_of_pos
nonneg_of_mul_nonneg_right 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Preorder.toLT	—	—	le_of_not_gt LT.lt.not_ge mul_neg_of_pos_of_neg
nonneg_of_mul_nonpos_left 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Preorder.toLT	—	—	le_of_not_gt LT.lt.not_ge mul_pos_of_neg_of_neg covariant_lt_of_contravariant_le contravariant_lt_of_covariant_le
nonneg_of_mul_nonpos_right 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Preorder.toLT	—	—	le_of_not_gt LT.lt.not_ge mul_pos_of_neg_of_neg covariant_lt_of_contravariant_le contravariant_lt_of_covariant_le
nonpos_of_mul_nonneg_left 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Preorder.toLT	—	—	le_of_not_gt LT.lt.not_ge mul_neg_of_pos_of_neg
nonpos_of_mul_nonneg_right 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Preorder.toLT	—	—	le_of_not_gt LT.lt.not_ge mul_neg_of_neg_of_pos
nonpos_of_mul_nonpos_left 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Preorder.toLT	—	—	le_of_not_gt LT.lt.not_ge mul_pos
nonpos_of_mul_nonpos_right 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Preorder.toLT	—	—	le_of_not_gt LT.lt.not_ge mul_pos
pos_iff_neg_of_mul_neg 📖	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—	neg_of_mul_neg_right le_of_lt pos_of_mul_neg_left
pos_of_left_mul_lt_le 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Preorder.toLE	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
pos_of_mul_neg_left 📖	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Preorder.toLE	—	—	lt_of_not_ge LE.le.not_gt mul_nonneg_of_nonpos_of_nonpos
pos_of_mul_neg_right 📖	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Preorder.toLE	—	—	lt_of_not_ge LE.le.not_gt mul_nonneg_of_nonpos_of_nonpos
pos_of_right_mul_lt_le 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Preorder.toLE	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
pow_two_nonneg 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	sq_nonneg
sign_cases_of_C_mul_pow_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	Preorder.toLT	—	pow_zero mul_one nonneg_of_mul_nonneg_right pow_one LE.le.eq_or_lt'
sq_nonneg 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	le_or_gt pow_succ_nonneg ExistsAddOfLE.exists_add_of_le LT.lt.le not_le LT.lt.ne' add_neg_of_neg_of_nonpos MulZeroClass.mul_zero add_zero add_mul Distrib.rightDistribClass mul_add Distrib.leftDistribClass sq add_comm add_assoc MulZeroClass.zero_mul
sq_nonpos_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	le_antisymm_iff sq_nonneg sq_eq_zero_iff isReduced_of_noZeroDivisors
strictAnti_mul_left 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	StrictAnti Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_lt_mul_of_neg_left
strictAnti_mul_right 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	StrictAnti Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_lt_mul_of_neg_right
sub_mul_sub_neg_iff 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLT Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	mul_neg_iff contravariant_lt_of_covariant_le IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add sub_neg LE.le.trans_lt LE.le.trans_lt'
sub_mul_sub_nonneg_iff 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	mul_nonneg_iff AddGroup.existsAddOfLE IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le sub_nonneg covariant_swap_add_of_covariant_add sub_nonpos LE.le.trans LE.le.trans'
sub_mul_sub_nonpos_iff 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	mul_nonpos_iff IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le sub_nonneg covariant_swap_add_of_covariant_add sub_nonpos LE.le.trans LE.le.trans'
sub_mul_sub_pos_iff 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLT MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	mul_pos_iff AddGroup.existsAddOfLE IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add sub_neg LE.le.trans_lt LE.le.trans_lt'
sub_one_lt 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	sub_lt_iff_lt_add covariant_swap_add_of_covariant_add lt_add_one
two_mul_le_add_of_sq_eq_mul 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.instAtLeastTwoHAddOfNat Distrib.toAdd	—	nonneg_le_nonneg_of_sq_le_sq MulPosStrictMono.toMulPosMono Nat.instAtLeastTwoHAddOfNat Left.add_nonneg pow_two mul_mul_mul_comm two_mul two_add_two_eq_four mul_assoc four_mul_le_sq_add
two_mul_le_add_pow_two 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.instAtLeastTwoHAddOfNat Distrib.toAdd Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	two_mul_le_add_sq
two_mul_le_add_sq 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.instAtLeastTwoHAddOfNat Distrib.toAdd Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Nat.instAtLeastTwoHAddOfNat two_mul add_mul Distrib.rightDistribClass sq min_mul_max max_mul_min fn_min_add_fn_max mul_add_mul_le_mul_add_mul MulPosStrictMono.toMulPosMono min_le_max

---

← Back to Index