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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoid.toNSMul 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoid.toNSMul 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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.toNSMul 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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.toNSMul 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	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring 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 instReflLe 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	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finset.card	—	zero_add pow_one pow_zero Finset.sum_congr one_mul instReflLe 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.toPow 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.toPow 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 instReflLe 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