Documentation Verification Report

Constructions

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

Statistics

Metric	Count
Definitions	0
Theorems `of_sigma`, `prodMk`, `prod_fiberwise`, `sigma`, `sigma_of_hasProd`, `sum`, `tprod_fiberwise`, `of_sigma`, `op`, `prodMk`, `prod_fiberwise`, `sigma`, `sigma_of_hasSum`, `sum`, `tsum_fiberwise`, `unop`, `prod`, `prod_factor`, `prod_symm`, `sigma`, `sigma'`, `sigma_factor`, `sum`, `tprod_comm`, `tprod_comm'`, `tprod_prod`, `tprod_prod'`, `tprod_prod_uncurry`, `tprod_sigma`, `tprod_sigma'`, `tprod_sum`, `hasProd`, `hasSum`, `multipliable`, `summable`, `ofStar`, `op`, `prod`, `prod_factor`, `prod_symm`, `sigma`, `sigma'`, `sigma_factor`, `sum`, `tsum_comm`, `tsum_comm'`, `tsum_prod`, `tsum_prod'`, `tsum_prod_uncurry`, `tsum_sigma`, `tsum_sigma'`, `tsum_sum`, `unop`, `hasProd_pi_single`, `hasSum_op`, `hasSum_pi_single`, `hasSum_unop`, `summable_op`, `summable_star_iff`, `summable_star_iff'`, `summable_unop`, `tprod_apply`, `tprod_pi_single`, `tprod_setProd_singleton_left`, `tprod_setProd_singleton_right`, `tsum_apply`, `tsum_op`, `tsum_pi_single`, `tsum_setProd_singleton_left`, `tsum_setProd_singleton_right`, `tsum_star`, `tsum_unop`	72
Total	72

HasProd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_sigma` 📖	—	`HasProd` `CommGroup.toCommMonoid` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional` `CauchySeq` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder` `Finset.prod`	—	—	`le_nhds_of_cauchy_adhp` `Finset.isDirected_le` `mem_nhds_iff` `IsOpen.mem_nhds` `Filter.Eventually.exists` `Filter.atTop_neBot` `Filter.Eventually.and` `Filter.Ici_mem_atTop` `Function.Injective.injOn` `sigma_mk_injective` `Finset.prod_congr` `Finset.prod_sigma` `tendsto_finset_prod` `IsTopologicalGroup.toContinuousMul` `IsUniformGroup.to_topologicalGroup` `Filter.Tendsto.comp` `Filter.tendsto_finset_preimage_atTop_atTop` `Filter.Tendsto.eventually_mem` `Finset.mem_image_of_mem`
`prodMk` 📖	mathematical	`HasProd`	`Prod.instCommMonoid` `instTopologicalSpaceProd`	—	`Finset.prod_congr` `Filter.Tendsto.prodMk_nhds`
`prod_fiberwise` 📖	—	`HasProd` `SummationFilter.unconditional`	—	—	`sigma` `Equiv.hasProd_iff`
`sigma` 📖	—	`HasProd` `SummationFilter.unconditional`	—	—	`Filter.HasBasis.tendsto_iff` `Filter.atTop_basis` `Finset.isDirected_le` `closed_nhds_basis` `Filter.mem_atTop_sets` `Function.Injective.injOn` `sigma_mk_injective` `Finset.prod_congr` `Finset.prod_sigma` `tendsto_finset_prod` `Filter.Tendsto.comp` `Filter.tendsto_finset_preimage_atTop_atTop` `IsClosed.mem_of_tendsto` `Filter.atTop_neBot` `Filter.eventually_atTop` `Finset.mem_filter` `Finset.mem_image_of_mem`
`sigma_of_hasProd` 📖	—	`HasProd` `SummationFilter.unconditional` `Multipliable`	—	—	`unique` `T25Space.t2Space` `T3Space.t25Space` `SummationFilter.instNeBotUnconditional` `sigma` `T3Space.toRegularSpace` `Multipliable.hasProd`
`sum` 📖	mathematical	`HasProd` `SummationFilter.unconditional`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	`OrderIso.map_atTop` `Filter.prod_atTop_atTop_eq` `Finset.prod_disjSum` `Finset.prod_congr` `Filter.Tendsto.comp` `tendsto_mul` `Filter.Tendsto.prodMap` `nhds_prod_eq`
`tprod_fiberwise` 📖	mathematical	`HasProd` `CommGroup.toCommMonoid` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	`tprod` `Set.Elem` `Set.preimage` `Set` `Set.instSingletonSet` `Set.instMembership`	—	`sigma` `IsTopologicalGroup.toContinuousMul` `IsUniformGroup.to_topologicalGroup` `IsTopologicalGroup.regularSpace` `Equiv.hasProd_iff` `Multipliable.hasProd_iff` `SummationFilter.instNeBotUnconditional` `Multipliable.subtype` `multipliable`

HasSum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_sigma` 📖	—	`HasSum` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional` `CauchySeq` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder` `Finset.sum`	—	—	`le_nhds_of_cauchy_adhp` `mapClusterPt_def` `mapClusterPt_iff_frequently` `Filter.frequently_atTop` `Finset.isDirected_le` `mem_nhds_iff` `IsOpen.mem_nhds` `Filter.Eventually.exists` `Filter.atTop_neBot` `Filter.Eventually.and` `Filter.Ici_mem_atTop` `Function.Injective.injOn` `sigma_mk_injective` `Finset.sum_congr` `Finset.sum_sigma` `tendsto_finset_sum` `IsTopologicalAddGroup.toContinuousAdd` `IsUniformAddGroup.to_topologicalAddGroup` `Filter.Tendsto.comp` `Filter.tendsto_finset_preimage_atTop_atTop` `Filter.Tendsto.eventually_mem` `Finset.mem_filter` `Finset.mem_image_of_mem`
`op` 📖	mathematical	`HasSum`	`MulOpposite` `MulOpposite.instAddCommMonoid` `MulOpposite.instTopologicalSpaceMulOpposite` `MulOpposite.op`	—	`map` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `MulOpposite.continuous_op`
`prodMk` 📖	mathematical	`HasSum`	`Prod.instAddCommMonoid` `instTopologicalSpaceProd`	—	`Finset.sum_congr` `prod_mk_sum` `Filter.Tendsto.prodMk_nhds`
`prod_fiberwise` 📖	—	`HasSum` `SummationFilter.unconditional`	—	—	`sigma` `Equiv.hasSum_iff`
`sigma` 📖	—	`HasSum` `SummationFilter.unconditional`	—	—	`Filter.HasBasis.tendsto_iff` `Filter.atTop_basis` `Finset.isDirected_le` `closed_nhds_basis` `Filter.mem_atTop_sets` `Function.Injective.injOn` `sigma_mk_injective` `Finset.sum_congr` `Finset.sum_sigma` `tendsto_finset_sum` `Filter.Tendsto.comp` `Filter.tendsto_finset_preimage_atTop_atTop` `IsClosed.mem_of_tendsto` `Filter.atTop_neBot` `Filter.eventually_atTop` `Finset.le_iff_subset` `Set.mem_preimage` `Finset.mem_filter` `Finset.mem_image_of_mem`
`sigma_of_hasSum` 📖	—	`HasSum` `SummationFilter.unconditional` `Summable`	—	—	`unique` `T25Space.t2Space` `T3Space.t25Space` `SummationFilter.instNeBotUnconditional` `sigma` `T3Space.toRegularSpace` `Summable.hasSum`
`sum` 📖	mathematical	`HasSum` `SummationFilter.unconditional`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`OrderIso.map_atTop` `Filter.prod_atTop_atTop_eq` `Finset.sum_disjSum` `Finset.sum_congr` `Filter.Tendsto.comp` `tendsto_add` `Filter.Tendsto.prodMap` `nhds_prod_eq` `Filter.map_map`
`tsum_fiberwise` 📖	mathematical	`HasSum` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	`tsum` `Set.Elem` `Set.preimage` `Set` `Set.instSingletonSet` `Set.instMembership`	—	`sigma` `IsTopologicalAddGroup.toContinuousAdd` `IsUniformAddGroup.to_topologicalAddGroup` `IsTopologicalAddGroup.regularSpace` `Equiv.hasSum_iff` `Summable.hasSum_iff` `SummationFilter.instNeBotUnconditional` `Summable.subtype` `summable`
`unop` 📖	mathematical	`HasSum` `MulOpposite` `MulOpposite.instAddCommMonoid` `MulOpposite.instTopologicalSpaceMulOpposite`	`MulOpposite.unop`	—	`map` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `MulOpposite.continuous_unop`

Multipliable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod` 📖	mathematical	`Multipliable` `CommGroup.toCommMonoid` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	`tprod`	—	`sigma` `Equiv.multipliable_iff`
`prod_factor` 📖	—	`Multipliable` `CommGroup.toCommMonoid` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	—	`comp_injective`
`prod_symm` 📖	—	`Multipliable` `SummationFilter.unconditional`	—	—	`Equiv.multipliable_iff`
`sigma` 📖	mathematical	`Multipliable` `CommGroup.toCommMonoid` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	`tprod`	—	`sigma'` `IsTopologicalGroup.toContinuousMul` `IsUniformGroup.to_topologicalGroup` `IsTopologicalGroup.regularSpace` `sigma_factor`
`sigma'` 📖	mathematical	`Multipliable` `SummationFilter.unconditional`	`tprod`	—	`HasProd.multipliable` `HasProd.sigma` `hasProd`
`sigma_factor` 📖	—	`Multipliable` `CommGroup.toCommMonoid` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	—	`comp_injective` `sigma_mk_injective`
`sum` 📖	—	`Multipliable` `SummationFilter.unconditional`	—	—	`HasProd.sum` `hasProd`
`tprod_comm` 📖	mathematical	`Multipliable` `CommGroup.toCommMonoid` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	`tprod`	—	`tprod_comm'` `IsTopologicalGroup.toContinuousMul` `IsUniformGroup.to_topologicalGroup` `instT3Space` `IsTopologicalGroup.regularSpace` `prod_factor` `prod_symm`
`tprod_comm'` 📖	mathematical	`Multipliable` `SummationFilter.unconditional`	`tprod`	—	`tprod_prod_uncurry` `prod_symm` `Equiv.tprod_eq`
`tprod_prod` 📖	mathematical	`Multipliable` `CommGroup.toCommMonoid` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	`tprod`	—	`tprod_prod'` `IsTopologicalGroup.toContinuousMul` `IsUniformGroup.to_topologicalGroup` `instT3Space` `IsTopologicalGroup.regularSpace` `prod_factor`
`tprod_prod'` 📖	mathematical	`Multipliable` `SummationFilter.unconditional`	`tprod`	—	`HasProd.tprod_eq` `T25Space.t2Space` `T3Space.t25Space` `SummationFilter.instNeBotUnconditional` `HasProd.prod_fiberwise` `T3Space.toRegularSpace` `hasProd`
`tprod_prod_uncurry` 📖	mathematical	`Multipliable` `SummationFilter.unconditional`	`tprod`	—	`HasProd.tprod_eq` `T25Space.t2Space` `T3Space.t25Space` `SummationFilter.instNeBotUnconditional` `HasProd.prod_fiberwise` `T3Space.toRegularSpace` `hasProd`
`tprod_sigma` 📖	mathematical	`Multipliable` `CommGroup.toCommMonoid` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	`tprod`	—	`tprod_sigma'` `IsTopologicalGroup.toContinuousMul` `IsUniformGroup.to_topologicalGroup` `instT3Space` `IsTopologicalGroup.regularSpace` `sigma_factor`
`tprod_sigma'` 📖	mathematical	`Multipliable` `SummationFilter.unconditional`	`tprod`	—	`HasProd.tprod_eq` `T25Space.t2Space` `T3Space.t25Space` `SummationFilter.instNeBotUnconditional` `HasProd.sigma` `T3Space.toRegularSpace` `hasProd`
`tprod_sum` 📖	mathematical	`Multipliable` `SummationFilter.unconditional`	`tprod` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	`HasProd.tprod_eq` `SummationFilter.instNeBotUnconditional` `HasProd.sum` `hasProd`

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasProd` 📖	mathematical	—	`HasProd` `commMonoid` `topologicalSpace`	—	`Finset.prod_apply` `Finset.prod_congr`
`hasSum` 📖	mathematical	—	`HasSum` `addCommMonoid` `topologicalSpace`	—	`tendsto_pi_nhds` `Finset.sum_apply` `Finset.sum_congr`
`multipliable` 📖	mathematical	—	`Multipliable` `commMonoid` `topologicalSpace`	—	—
`summable` 📖	mathematical	—	`Summable` `addCommMonoid` `topologicalSpace`	—	`hasSum`

Summable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofStar` 📖	—	`Summable` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid`	—	—	`star_star` `star`
`op` 📖	mathematical	`Summable`	`MulOpposite` `MulOpposite.instAddCommMonoid` `MulOpposite.instTopologicalSpaceMulOpposite` `MulOpposite.op`	—	`HasSum.summable` `HasSum.op` `hasSum`
`prod` 📖	mathematical	`Summable` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	`tsum`	—	`sigma` `Equiv.summable_iff`
`prod_factor` 📖	—	`Summable` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	—	`comp_injective`
`prod_symm` 📖	—	`Summable` `SummationFilter.unconditional`	—	—	`Equiv.summable_iff`
`sigma` 📖	mathematical	`Summable` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	`tsum`	—	`sigma'` `IsTopologicalAddGroup.toContinuousAdd` `IsUniformAddGroup.to_topologicalAddGroup` `IsTopologicalAddGroup.regularSpace` `sigma_factor`
`sigma'` 📖	mathematical	`Summable` `SummationFilter.unconditional`	`tsum`	—	`HasSum.summable` `HasSum.sigma` `hasSum`
`sigma_factor` 📖	—	`Summable` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	—	—	`comp_injective` `sigma_mk_injective`
`sum` 📖	—	`Summable` `SummationFilter.unconditional`	—	—	`HasSum.sum` `hasSum`
`tsum_comm` 📖	mathematical	`Summable` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	`tsum`	—	`tsum_comm'` `IsTopologicalAddGroup.toContinuousAdd` `IsUniformAddGroup.to_topologicalAddGroup` `instT3Space` `IsTopologicalAddGroup.regularSpace` `prod_factor` `prod_symm`
`tsum_comm'` 📖	mathematical	`Summable` `SummationFilter.unconditional`	`tsum`	—	`tsum_prod_uncurry` `prod_symm` `Equiv.tsum_eq`
`tsum_prod` 📖	mathematical	`Summable` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	`tsum`	—	`tsum_prod'` `IsTopologicalAddGroup.toContinuousAdd` `IsUniformAddGroup.to_topologicalAddGroup` `instT3Space` `IsTopologicalAddGroup.regularSpace` `prod_factor`
`tsum_prod'` 📖	mathematical	`Summable` `SummationFilter.unconditional`	`tsum`	—	`HasSum.tsum_eq` `T25Space.t2Space` `T3Space.t25Space` `SummationFilter.instNeBotUnconditional` `HasSum.prod_fiberwise` `T3Space.toRegularSpace` `hasSum`
`tsum_prod_uncurry` 📖	mathematical	`Summable` `SummationFilter.unconditional`	`tsum`	—	`HasSum.tsum_eq` `T25Space.t2Space` `T3Space.t25Space` `SummationFilter.instNeBotUnconditional` `HasSum.prod_fiberwise` `T3Space.toRegularSpace` `hasSum`
`tsum_sigma` 📖	mathematical	`Summable` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `SummationFilter.unconditional`	`tsum`	—	`tsum_sigma'` `IsTopologicalAddGroup.toContinuousAdd` `IsUniformAddGroup.to_topologicalAddGroup` `instT3Space` `IsTopologicalAddGroup.regularSpace` `sigma_factor`
`tsum_sigma'` 📖	mathematical	`Summable` `SummationFilter.unconditional`	`tsum`	—	`HasSum.tsum_eq` `T25Space.t2Space` `T3Space.t25Space` `SummationFilter.instNeBotUnconditional` `HasSum.sigma` `T3Space.toRegularSpace` `hasSum`
`tsum_sum` 📖	mathematical	`Summable` `SummationFilter.unconditional`	`tsum` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`HasSum.tsum_eq` `SummationFilter.instNeBotUnconditional` `HasSum.sum` `hasSum`
`unop` 📖	mathematical	`Summable` `MulOpposite` `MulOpposite.instAddCommMonoid` `MulOpposite.instTopologicalSpaceMulOpposite`	`MulOpposite.unop`	—	`HasSum.summable` `HasSum.unop` `hasSum`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasProd_pi_single` 📖	mathematical	—	`HasProd` `Pi.mulSingle` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SummationFilter.unconditional`	—	`Pi.mulSingle_apply` `hasProd_ite_eq` `SummationFilter.instLeAtTopUnconditional`
`hasSum_op` 📖	mathematical	—	`HasSum` `MulOpposite` `MulOpposite.instAddCommMonoid` `MulOpposite.instTopologicalSpaceMulOpposite` `MulOpposite.op`	—	`HasSum.unop` `HasSum.op`
`hasSum_pi_single` 📖	mathematical	—	`HasSum` `Pi.single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SummationFilter.unconditional`	—	`Pi.single_apply` `hasSum_ite_eq` `SummationFilter.instLeAtTopUnconditional`
`hasSum_unop` 📖	mathematical	—	`HasSum` `MulOpposite.unop` `MulOpposite` `MulOpposite.instAddCommMonoid` `MulOpposite.instTopologicalSpaceMulOpposite`	—	`HasSum.op` `HasSum.unop`
`summable_op` 📖	mathematical	—	`Summable` `MulOpposite` `MulOpposite.instAddCommMonoid` `MulOpposite.instTopologicalSpaceMulOpposite` `MulOpposite.op`	—	`Summable.unop` `Summable.op`
`summable_star_iff` 📖	mathematical	—	`Summable` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid`	—	`Summable.ofStar` `Summable.star`
`summable_star_iff'` 📖	mathematical	—	`Summable` `Star.star` `Pi.instStarForall` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid`	—	`summable_star_iff`
`summable_unop` 📖	mathematical	—	`Summable` `MulOpposite.unop` `MulOpposite` `MulOpposite.instAddCommMonoid` `MulOpposite.instTopologicalSpaceMulOpposite`	—	`Summable.op` `Summable.unop`
`tprod_apply` 📖	mathematical	`T2Space` `Multipliable` `Pi.commMonoid` `Pi.topologicalSpace`	`tprod`	—	`HasProd.tprod_eq` `Pi.hasProd` `Multipliable.hasProd`
`tprod_pi_single` 📖	mathematical	—	`tprod` `Pi.mulSingle` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `SummationFilter.unconditional`	—	`tprod_eq_mulSingle` `SummationFilter.instLeAtTopUnconditional` `Pi.mulSingle_eq_of_ne` `Pi.mulSingle_eq_same`
`tprod_setProd_singleton_left` 📖	mathematical	—	`tprod` `Set.Elem` `SProd.sprod` `Set` `Set.instSProd` `Set.instSingletonSet` `Set.instMembership` `SummationFilter.unconditional`	—	`tprod_congr_set_coe` `Set.singleton_prod` `tprod_image` `Function.Injective.injOn` `Prod.mk_right_injective`
`tprod_setProd_singleton_right` 📖	mathematical	—	`tprod` `Set.Elem` `SProd.sprod` `Set` `Set.instSProd` `Set.instSingletonSet` `Set.instMembership` `SummationFilter.unconditional`	—	`tprod_congr_set_coe` `Set.prod_singleton` `tprod_image` `Function.Injective.injOn` `Prod.mk_left_injective`
`tsum_apply` 📖	mathematical	`T2Space` `Summable` `Pi.addCommMonoid` `Pi.topologicalSpace`	`tsum`	—	`HasSum.tsum_eq` `Pi.hasSum` `Summable.hasSum`
`tsum_op` 📖	mathematical	—	`tsum` `MulOpposite` `MulOpposite.instAddCommMonoid` `MulOpposite.instTopologicalSpaceMulOpposite` `MulOpposite.op`	—	`Topology.IsClosedEmbedding.map_tsum` `MulOpposite.instT2Space` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `Homeomorph.isClosedEmbedding`
`tsum_pi_single` 📖	mathematical	—	`tsum` `Pi.single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SummationFilter.unconditional`	—	`tsum_eq_single` `SummationFilter.instLeAtTopUnconditional` `Pi.single_eq_of_ne` `Pi.single_eq_same`
`tsum_setProd_singleton_left` 📖	mathematical	—	`tsum` `Set.Elem` `SProd.sprod` `Set` `Set.instSProd` `Set.instSingletonSet` `Set.instMembership` `SummationFilter.unconditional`	—	`tsum_congr_set_coe` `Set.singleton_prod` `tsum_image` `Function.Injective.injOn` `Prod.mk_right_injective`
`tsum_setProd_singleton_right` 📖	mathematical	—	`tsum` `Set.Elem` `SProd.sprod` `Set` `Set.instSProd` `Set.instSingletonSet` `Set.instMembership` `SummationFilter.unconditional`	—	`tsum_congr_set_coe` `Set.prod_singleton` `tsum_image` `Function.Injective.injOn` `Prod.mk_left_injective`
`tsum_star` 📖	mathematical	—	`Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `tsum`	—	`Function.LeftInverse.map_tsum` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `ContinuousStar.continuous_star` `star_star`
`tsum_unop` 📖	mathematical	—	`tsum` `MulOpposite.unop` `MulOpposite` `MulOpposite.instAddCommMonoid` `MulOpposite.instTopologicalSpaceMulOpposite`	—	`MulOpposite.op_injective` `tsum_op`

---

← Back to Index