GroupCompletion

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

Statistics

Metric	Count
Definitions	0
Theorems toCompl_tsum, hasSum_iff_hasSum_compl, summable_iff_cauchySeq_finset_and_tsum_mem, summable_iff_summable_compl_and_tsum_mem	4
Total	4

Summable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toCompl_tsum 📖	mathematical	Summable AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace	tsum UniformSpace.Completion UniformSpace.Completion.instAddCommGroup UniformSpace.Completion.uniformSpace DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup UniformSpace.Completion.instAddMonoid AddMonoidHom.instFunLike UniformSpace.Completion.toCompl UniformSpace.Completion.coe'	—	map_tsum T25Space.t2Space T3Space.t25Space instT3Space UniformSpace.Completion.t0Space IsTopologicalAddGroup.regularSpace IsUniformAddGroup.to_topologicalAddGroup UniformSpace.Completion.isUniformAddGroup AddMonoidHom.instAddMonoidHomClass UniformSpace.Completion.continuous_coe

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasSum_iff_hasSum_compl 📖	mathematical	—	HasSum UniformSpace.Completion AddCommGroup.toAddCommMonoid UniformSpace.Completion.instAddCommGroup UniformSpace.toTopologicalSpace UniformSpace.Completion.uniformSpace DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup UniformSpace.Completion.instAddMonoid AddMonoidHom.instFunLike UniformSpace.Completion.toCompl UniformSpace.Completion.coe'	—	Topology.IsInducing.hasSum_iff AddMonoidHom.instAddMonoidHomClass IsDenseInducing.toIsInducing UniformSpace.Completion.isDenseInducing_toCompl
summable_iff_cauchySeq_finset_and_tsum_mem 📖	mathematical	—	Summable AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace SummationFilter.unconditional CauchySeq Finset PartialOrder.toPreorder Finset.partialOrder Finset.sum UniformSpace.Completion Set Set.instMembership Set.range DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup UniformSpace.Completion.instAddMonoid AddMonoidHom.instFunLike UniformSpace.Completion.toCompl tsum UniformSpace.Completion.instAddCommGroup UniformSpace.Completion.uniformSpace	—	Filter.Tendsto.cauchySeq summable_iff_summable_compl_and_tsum_mem summable_iff_cauchySeq_finset UniformSpace.Completion.completeSpace Finset.sum_congr AddMonoidHom.instAddMonoidHomClass Cauchy.map UniformSpace.Completion.uniformContinuous_coe
summable_iff_summable_compl_and_tsum_mem 📖	mathematical	—	Summable AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace UniformSpace.Completion UniformSpace.Completion.instAddCommGroup UniformSpace.Completion.uniformSpace DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup UniformSpace.Completion.instAddMonoid AddMonoidHom.instFunLike UniformSpace.Completion.toCompl Set Set.instMembership Set.range tsum	—	Topology.IsInducing.summable_iff_tsum_comp_mem_range T25Space.t2Space T3Space.t25Space instT3Space UniformSpace.Completion.t0Space IsTopologicalAddGroup.regularSpace IsUniformAddGroup.to_topologicalAddGroup UniformSpace.Completion.isUniformAddGroup AddMonoidHom.instAddMonoidHomClass IsDenseInducing.toIsInducing UniformSpace.Completion.isDenseInducing_toCompl

---

← Back to Index