Documentation Verification Report

Ring

📁 Source: Mathlib/Topology/Algebra/InfiniteSum/Ring.lean

Statistics

Metric	Count
Definitions	0
Theorems `tsum_left`, `tsum_right`, `const_div`, `div_const`, `mul`, `mul_eq`, `mul_left`, `mul_right`, `const_div`, `div_const`, `mul_left`, `mul_right`, `one_sub_mul_tsum_pow`, `tsum_mul_left`, `tsum_mul_right`, `tsum_mul_tsum`, `tsum_mul_tsum_eq_tsum_sum_antidiagonal`, `tsum_mul_tsum_eq_tsum_sum_range`, `tsum_pow_mul_one_sub`, `hasProd_one_add_of_hasSum_prod`, `hasSum_const_div_iff`, `hasSum_div_const_iff`, `hasSum_mul_left_iff`, `hasSum_mul_right_iff`, `multipliable_one_add_of_summable_prod`, `summable_const_div_iff`, `summable_div_const_iff`, `summable_mul_left_iff`, `summable_mul_prod_iff_summable_mul_sigma_antidiagonal`, `summable_mul_right_iff`, `summable_sum_mul_antidiagonal_of_summable_mul`, `summable_sum_mul_range_of_summable_mul`, `tprod_one_add`, `tprod_one_add_ordered`, `tprod_one_sub_ordered`, `tsum_div_const`, `tsum_mul_left`, `tsum_mul_right`	38
Total	38

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tsum_left` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`tsum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`symm` `tsum_right`
`tsum_right` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`tsum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`Summable.tsum_mul_left` `tsum_congr` `Summable.tsum_mul_right` `zero_right` `tsum_eq_zero_of_not_summable`

HasSum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_div` 📖	mathematical	`HasSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_left` `div_eq_mul_inv` `one_mul`
`div_const` 📖	mathematical	`HasSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring`	`DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero`	—	`div_eq_mul_inv` `mul_right`
`mul` 📖	—	`HasSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `SummationFilter.unconditional` `Summable` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—	`mul_eq`
`mul_eq` 📖	—	`HasSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `SummationFilter.unconditional` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—	`mul_right` `mul_left` `prod_fiberwise` `IsTopologicalSemiring.toContinuousAdd` `T3Space.toRegularSpace` `unique` `T25Space.t2Space` `T3Space.t25Space` `SummationFilter.instNeBotUnconditional`
`mul_left` 📖	mathematical	`HasSum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`map` `AddMonoidHom.instAddMonoidHomClass` `Continuous.mul` `IsTopologicalSemiring.toContinuousMul` `continuous_const` `continuous_id`
`mul_right` 📖	mathematical	`HasSum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`map` `AddMonoidHom.instAddMonoidHomClass` `Continuous.mul` `IsTopologicalSemiring.toContinuousMul` `continuous_id` `continuous_const`

Summable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_div` 📖	—	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—	`HasSum.summable` `HasSum.const_div` `hasSum`
`div_const` 📖	mathematical	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring`	`DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero`	—	`HasSum.summable` `HasSum.div_const` `hasSum`
`mul_left` 📖	mathematical	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`HasSum.summable` `HasSum.mul_left` `hasSum`
`mul_right` 📖	mathematical	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`HasSum.summable` `HasSum.mul_right` `hasSum`
`one_sub_mul_tsum_pow` 📖	mathematical	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SummationFilter.unconditional`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `tsum`	—	`tendsto_nhds_unique` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `HasSum.tendsto_sum_nat` `HasSum.mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `hasSum` `mul_neg_geom_sum` `sub_zero` `Filter.Tendsto.sub` `IsTopologicalAddGroup.to_continuousSub` `IsTopologicalRing.to_topologicalAddGroup` `tendsto_const_nhds` `tendsto_atTop_zero`
`tsum_mul_left` 📖	mathematical	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid`	`tsum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`HasSum.tsum_eq` `HasSum.mul_left` `hasSum`
`tsum_mul_right` 📖	mathematical	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid`	`tsum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`HasSum.tsum_eq` `HasSum.mul_right` `hasSum`
`tsum_mul_tsum` 📖	mathematical	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid` `SummationFilter.unconditional` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`tsum`	—	`HasSum.mul_eq` `hasSum`
`tsum_mul_tsum_eq_tsum_sum_antidiagonal` 📖	mathematical	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid` `SummationFilter.unconditional` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`tsum` `Finset.sum` `Finset.HasAntidiagonal.antidiagonal` `AddCommMonoid.toAddMonoid`	—	`Finset.sum_finset_coe` `tsum_fintype` `SummationFilter.instLeAtTopUnconditional` `tsum_mul_tsum` `Equiv.tsum_eq` `tsum_sigma'` `IsTopologicalSemiring.toContinuousAdd` `HasSum.summable` `hasSum_fintype` `summable_mul_prod_iff_summable_mul_sigma_antidiagonal`
`tsum_mul_tsum_eq_tsum_sum_range` 📖	mathematical	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid` `SummationFilter.unconditional` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`tsum` `Finset.sum` `Finset.range`	—	`Finset.Nat.sum_antidiagonal_eq_sum_range_succ` `tsum_mul_tsum_eq_tsum_sum_antidiagonal`
`tsum_pow_mul_one_sub` 📖	mathematical	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SummationFilter.unconditional`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `tsum` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`tendsto_nhds_unique` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `HasSum.tendsto_sum_nat` `HasSum.mul_right` `IsTopologicalRing.toIsTopologicalSemiring` `hasSum` `geom_sum_mul_neg` `sub_zero` `Filter.Tendsto.sub` `IsTopologicalAddGroup.to_continuousSub` `IsTopologicalRing.to_topologicalAddGroup` `tendsto_const_nhds` `tendsto_atTop_zero`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasProd_one_add_of_hasSum_prod` 📖	mathematical	`HasSum` `Finset` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finset.prod` `CommSemiring.toCommMonoid` `SummationFilter.unconditional`	`HasProd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Finset.prod_congr` `Finset.prod_one_add` `Filter.Tendsto.comp` `Filter.tendsto_finset_powerset_atTop_atTop`
`hasSum_const_div_iff` 📖	mathematical	—	`HasSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Pi.instDiv` `Pi.instOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`div_eq_mul_inv` `one_mul` `hasSum_mul_left_iff`
`hasSum_div_const_iff` 📖	mathematical	—	`HasSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero`	—	`div_eq_mul_inv` `hasSum_mul_right_iff` `inv_ne_zero`
`hasSum_mul_left_iff` 📖	mathematical	—	`HasSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`inv_mul_cancel_left₀` `HasSum.mul_left`
`hasSum_mul_right_iff` 📖	mathematical	—	`HasSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_inv_cancel_right₀` `HasSum.mul_right`
`multipliable_one_add_of_summable_prod` 📖	mathematical	`Summable` `Finset` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finset.prod` `CommSemiring.toCommMonoid` `SummationFilter.unconditional`	`Multipliable` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`hasProd_one_add_of_hasSum_prod`
`summable_const_div_iff` 📖	mathematical	—	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Pi.instDiv` `Pi.instOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`div_eq_mul_inv` `one_mul` `summable_mul_left_iff`
`summable_div_const_iff` 📖	mathematical	—	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero`	—	`div_eq_mul_inv` `summable_mul_right_iff` `inv_ne_zero`
`summable_mul_left_iff` 📖	mathematical	—	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`inv_mul_cancel_left₀` `Summable.mul_left`
`summable_mul_prod_iff_summable_mul_sigma_antidiagonal` 📖	mathematical	—	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `SummationFilter.unconditional` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.HasAntidiagonal.antidiagonal` `AddCommMonoid.toAddMonoid`	—	`Equiv.summable_iff`
`summable_mul_right_iff` 📖	mathematical	—	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_inv_cancel_right₀` `Summable.mul_right`
`summable_sum_mul_antidiagonal_of_summable_mul` 📖	mathematical	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `SummationFilter.unconditional`	`Finset.sum` `Finset.HasAntidiagonal.antidiagonal` `AddCommMonoid.toAddMonoid`	—	`Finset.sum_finset_coe` `tsum_fintype` `SummationFilter.instLeAtTopUnconditional` `Summable.sigma'` `IsTopologicalSemiring.toContinuousAdd` `T3Space.toRegularSpace` `summable_mul_prod_iff_summable_mul_sigma_antidiagonal` `HasSum.summable` `hasSum_fintype`
`summable_sum_mul_range_of_summable_mul` 📖	mathematical	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `SummationFilter.unconditional`	`Finset.sum` `Finset.range`	—	`Finset.Nat.sum_antidiagonal_eq_sum_range_succ` `summable_sum_mul_antidiagonal_of_summable_mul`
`tprod_one_add` 📖	mathematical	`Summable` `Finset` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finset.prod` `CommSemiring.toCommMonoid` `SummationFilter.unconditional`	`tprod` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `tsum`	—	`HasProd.tprod_eq` `SummationFilter.instNeBotUnconditional` `hasProd_one_add_of_hasSum_prod` `Summable.hasSum`
`tprod_one_add_ordered` 📖	mathematical	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Finset.prod` `CommSemiring.toCommMonoid` `Finset.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Distrib.toAdd` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `SummationFilter.unconditional` `Multipliable`	`tprod` `tsum`	—	`isEmpty_or_nonempty` `tprod_empty` `tsum_empty` `add_zero` `HasSum.tsum_eq` `SummationFilter.instNeBotUnconditional` `tendsto_nhds_unique` `Filter.atTop_neBot` `SemilatticeSup.instIsDirectedOrder` `Filter.Tendsto.comp` `Finset.prod_one_add_ordered` `Filter.tendsto_finset_Iic_atTop_atTop` `Filter.Tendsto.const_add` `Finset.sum_congr` `HasProd.tprod_eq`
`tprod_one_sub_ordered` 📖	mathematical	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Finset.prod` `CommRing.toCommMonoid` `Finset.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `SummationFilter.unconditional` `Multipliable`	`tprod` `tsum`	—	`sub_eq_add_neg` `Finset.prod_congr` `tprod_one_add_ordered` `IsTopologicalAddGroup.toContinuousAdd` `Summable.neg`
`tsum_div_const` 📖	mathematical	—	`tsum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero`	—	`div_eq_mul_inv` `tsum_mul_right`
`tsum_mul_left` 📖	mathematical	—	`tsum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`MulZeroClass.zero_mul` `tsum_zero` `Topology.IsClosedEmbedding.map_tsum` `AddMonoidHom.instAddMonoidHomClass` `Homeomorph.isClosedEmbedding` `IsTopologicalSemiring.toContinuousMul`
`tsum_mul_right` 📖	mathematical	—	`tsum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`MulZeroClass.mul_zero` `tsum_zero` `Topology.IsClosedEmbedding.map_tsum` `AddMonoidHom.instAddMonoidHomClass` `Homeomorph.isClosedEmbedding` `IsTopologicalSemiring.toContinuousMul`

---

← Back to Index