TsumDivisorsAntidiagonal

📁 Source: Mathlib/NumberTheory/TsumDivisorsAntidiagonal.lean

Statistics

Metric	Count
Definitions divisorsAntidiagonalFactors, sigmaAntidiagonalEquivProd	2
Theorems divisorsAntidiagonalFactors_eq, divisorsAntidiagonalFactors_one, sigmaAntidiagonalEquivProd_symm_apply_fst, sigmaAntidiagonalEquivProd_symm_apply_snd, summable_norm_pow_mul_geometric_div_one_sub, summable_prod_mul_pow, tendsto_zero_geometric_tsum_pnat, tsum_pow_div_one_sub_eq_tsum_sigma, tsum_prod_pow_eq_tsum_sigma	9
Total	11

(root)

Definitions

Name	Category	Theorems
divisorsAntidiagonalFactors 📖	CompOp	2 math math: divisorsAntidiagonalFactors_one, divisorsAntidiagonalFactors_eq
sigmaAntidiagonalEquivProd 📖	CompOp	2 math math: sigmaAntidiagonalEquivProd_symm_apply_snd, sigmaAntidiagonalEquivProd_symm_apply_fst

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
divisorsAntidiagonalFactors_eq 📖	mathematical	—	PNat divisorsAntidiagonalFactors PNat.val	—	Nat.mem_divisorsAntidiagonal
divisorsAntidiagonalFactors_one 📖	mathematical	—	divisorsAntidiagonalFactors PNat instOfNatPNatOfNeZeroNat	—	Nat.mem_divisorsAntidiagonal LT.lt.ne' Unique.instSubsingleton
sigmaAntidiagonalEquivProd_symm_apply_fst 📖	mathematical	—	PNat.val PNat Finset SetLike.instMembership Finset.instSetLike Nat.divisorsAntidiagonal DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm sigmaAntidiagonalEquivProd	—	—
sigmaAntidiagonalEquivProd_symm_apply_snd 📖	mathematical	—	Finset SetLike.instMembership Finset.instSetLike Nat.divisorsAntidiagonal PNat.val PNat DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm sigmaAntidiagonalEquivProd	—	—
summable_norm_pow_mul_geometric_div_one_sub 📖	mathematical	Real Real.instLT Norm.norm NormedField.toNorm NontriviallyNormedField.toNormedField Real.instOne	Summable ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup AddMonoidWithOne.toOne SummationFilter.unconditional	—	div_eq_mul_one_div Summable.mul_tendsto_const NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass norm_mul norm_pow summable_norm_pow_mul_geometric_of_norm_lt_one Nat.cofinite_eq_atTop Filter.Tendsto.div IsTopologicalDivisionRing.toContinuousInv₀ NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing tendsto_const_nhds Filter.Tendsto.const_sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup tendsto_pow_atTop_nhds_zero_of_norm_lt_one sub_zero NeZero.one IsSimpleRing.instNontrivial DivisionRing.isSimpleRing
summable_prod_mul_pow 📖	mathematical	Real Real.instLT Norm.norm NormedField.toNorm NontriviallyNormedField.toNormedField Real.instOne	Summable PNat ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing PNat.val SummationFilter.unconditional	—	Equiv.summable_iff
tendsto_zero_geometric_tsum_pnat 📖	mathematical	Real Real.instLT Norm.norm NormedField.toNorm NontriviallyNormedField.toNormedField Real.instOne	Filter.Tendsto PNat tsum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField PNat.val SummationFilter.unconditional Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderPNat nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing	—	norm_pow NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass pow_lt_one_iff_of_nonneg IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass norm_nonneg NeZero.pnat tsum_geometric_of_norm_lt_one tsum_zero_pnat_eq_tsum_nat SeminormedAddCommGroup.toIsTopologicalAddGroup TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace summable_geometric_of_norm_lt_one instHasSummableGeomSeries pow_zero add_sub_cancel_left mul_comm pow_mul sub_zero inv_one sub_self Filter.tendsto_sub_const_iff IsTopologicalAddGroup.to_continuousSub tendsto_inv_iff₀ IsTopologicalDivisionRing.toContinuousInv₀ NormedDivisionRing.to_isTopologicalDivisionRing NeZero.one IsSimpleRing.instNontrivial DivisionRing.isSimpleRing Filter.tendsto_const_sub_iff Filter.Tendsto.comp tendsto_pow_atTop_nhds_zero_of_norm_lt_one tendsto_PNat_val_atTop_atTop
tsum_pow_div_one_sub_eq_tsum_sigma 📖	mathematical	Real Real.instLT Norm.norm NormedField.toNorm NontriviallyNormedField.toNormedField Real.instOne	tsum PNat ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing PNat.val SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup AddMonoidWithOne.toOne SummationFilter.unconditional DFunLike.coe ArithmeticFunction MulZeroClass.toZero Nat.instMulZeroClass ArithmeticFunction.instFunLikeNat ArithmeticFunction.sigma	—	tsum_geometric_of_norm_lt_one norm_pow NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass pow_lt_one₀ IsOrderedRing.toPosMulMono Real.instIsOrderedRing div_eq_mul_inv NeZero.pnat IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace mul_assoc tsum_pnat_eq_tsum_succ tsum_prod_pow_eq_tsum_sigma Summable.tsum_comm SeminormedAddCommGroup.to_isUniformAddGroup T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity Summable.prod_symm summable_prod_mul_pow tsum_congr₂ mul_comm pow_mul
tsum_prod_pow_eq_tsum_sigma 📖	mathematical	Real Real.instLT Norm.norm NormedField.toNorm NontriviallyNormedField.toNormedField Real.instOne	tsum PNat ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing PNat.val SummationFilter.unconditional DFunLike.coe ArithmeticFunction MulZeroClass.toZero Nat.instMulZeroClass ArithmeticFunction.instFunLikeNat ArithmeticFunction.sigma	—	Equiv.tsum_eq Summable.tsum_sigma SeminormedAddCommGroup.to_isUniformAddGroup T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity ArithmeticFunction.sigma_eq_sum_div Nat.cast_sum Finset.sum_congr Nat.cast_pow tsum_congr tsum_fintype SummationFilter.instLeAtTopUnconditional Finset.sum_attach Nat.sum_divisorsAntidiagonal Finset.sum_mul Nat.dvd_of_mem_divisors Summable.tsum_prod summable_prod_mul_pow

---

← Back to Index