Chebyshev

📁 Source: Mathlib/Algebra/Order/Chebyshev.lean

Statistics

Metric	Count
Definitions	0
Theorems card_mul_sum_le_sum_mul_sum, card_smul_sum_le_sum_smul_sum, card_mul_sum_le_sum_mul_sum, card_smul_sum_le_sum_smul_sum, sum_mul_sum_le_card_mul_sum, sum_smul_sum_le_card_smul_sum, sum_mul_sum_le_card_mul_sum, sum_smul_sum_le_card_smul_sum, pow_sum_div_card_le_sum_pow, pow_sum_le_card_mul_sum_pow, sq_sum_le_card_mul_sum_sq, sum_div_card_sq_le_sum_sq_div_card	12
Total	12

Antivary

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_mul_sum_le_sum_mul_sum 📖	mathematical	Antivary PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLE Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Fintype.card Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.univ	—	AntivaryOn.card_mul_sum_le_sum_mul_sum antivaryOn
card_smul_sum_le_sum_smul_sum 📖	mathematical	Antivary PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLE AddMonoid.toNatSMul AddCommMonoid.toAddMonoid Fintype.card Finset.sum Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	MonovaryOn.sum_smul_sum_le_card_smul_sum OrderDual.isOrderedAddCancelMonoid OrderDual.instPosSMulMono Monovary.monovaryOn dual_right

AntivaryOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_mul_sum_le_sum_mul_sum 📖	mathematical	AntivaryOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SetLike.coe Finset Finset.instSetLike	Preorder.toLE Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finset.card Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid	—	nsmul_eq_mul card_smul_sum_le_sum_smul_sum IsStrictOrderedRing.toIsOrderedCancelAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule
card_smul_sum_le_sum_smul_sum 📖	mathematical	AntivaryOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SetLike.coe Finset Finset.instSetLike	Preorder.toLE AddMonoid.toNatSMul AddCommMonoid.toAddMonoid Finset.card Finset.sum SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	MonovaryOn.sum_smul_sum_le_card_smul_sum OrderDual.isOrderedAddCancelMonoid OrderDual.instPosSMulMono dual_right

Monovary

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sum_mul_sum_le_card_mul_sum 📖	mathematical	Monovary PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLE Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.univ AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Fintype.card	—	MonovaryOn.sum_mul_sum_le_card_mul_sum monovaryOn
sum_smul_sum_le_card_smul_sum 📖	mathematical	Monovary PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLE SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finset.univ AddMonoid.toNatSMul Fintype.card	—	MonovaryOn.sum_smul_sum_le_card_smul_sum monovaryOn

MonovaryOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sum_mul_sum_le_card_mul_sum 📖	mathematical	MonovaryOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SetLike.coe Finset Finset.instSetLike	Preorder.toLE Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finset.card	—	nsmul_eq_mul sum_smul_sum_le_card_smul_sum IsStrictOrderedRing.toIsOrderedCancelAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule
sum_smul_sum_le_card_smul_sum 📖	mathematical	MonovaryOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SetLike.coe Finset Finset.instSetLike	Preorder.toLE SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoid.toNatSMul Finset.card	—	Set.Countable.exists_cycleOn Finset.countable_toSet Finset.card_range Finset.sum_smul_sum_eq_sum_perm Finset.sum_le_card_nsmul IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid sum_smul_comp_perm_le_sum_smul Function.IsFixedPt.perm_pow

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pow_sum_div_card_le_sum_pow 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finset.card	—	Finset.eq_empty_or_nonempty zero_pow CharP.cast_eq_zero CharP.ofCharZero IsStrictOrderedRing.toCharZero zero_div div_le_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono pow_pos IsStrictOrderedRing.toZeroLEOneClass Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing NeZero.charZero_one Finset.Nonempty.card_pos pow_sum_le_card_mul_sum_pow
pow_sum_le_card_mul_sum_pow 📖	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 Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finset.card	—	zero_add pow_one pow_zero Finset.sum_congr one_mul pow_succ mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono IsStrictOrderedRing.toIsOrderedRing Finset.sum_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid mul_assoc mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono MonovaryOn.sum_mul_sum_le_card_mul_sum MonovaryOn.pow_left₀ monovaryOn_self pow_nonneg IsOrderedRing.toZeroLEOneClass Nat.cast_nonneg' IsStrictOrderedRing.toZeroLEOneClass
sq_sum_le_card_mul_sum_sq 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finset.card	—	sq Finset.sum_congr MonovaryOn.sum_mul_sum_le_card_mul_sum monovaryOn_self
sum_div_card_sq_le_sum_sq_div_card 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finset.card	—	Finset.eq_empty_or_nonempty CharP.cast_eq_zero CharP.ofCharZero IsStrictOrderedRing.toCharZero div_zero zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat div_pow div_le_div_iff₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono pow_pos IsStrictOrderedRing.toZeroLEOneClass Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing NeZero.charZero_one Finset.Nonempty.card_pos sq mul_left_comm mul_assoc mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono sq_sum_le_card_mul_sum_sq le_of_lt

---

← Back to Index