Documentation Verification Report

GroupCompletion

πŸ“ Source: Mathlib/Topology/Algebra/GroupCompletion.lean

Statistics

MetricCount
Definitionscompletion, extension, addGroup, instAddCommGroup, instAddMonoid, instDistribMulActionOfUniformContinuousConstSMul, instModule, instMulActionWithZeroOfUniformContinuousConstSMul, instSubNegMonoid, toCompl, instAddCompletion, instNegCompletion, instSubCompletion, instZeroCompletion
14
Theoremscompletion_add, completion_coe, completion_zero, continuous_completion, continuous_extension, extension_coe, coe_add, coe_eq_zero_iff, coe_neg, coe_sub, coe_zero, continuous_toCompl, isDenseInducing_toCompl, isUniformAddGroup, toCompl_apply
15
Total29

AddMonoidHom

Definitions

NameCategoryTheorems
completion πŸ“–CompOp
5 mathmath: completion_coe, continuous_completion, completion_add, ContinuousLinearMap.toAddMonoidHom_completion, completion_zero
extension πŸ“–CompOp
2 mathmath: extension_coe, continuous_extension

Theorems

NameKindAssumesProvesValidatesDepends On
completion_add πŸ“–mathematicalContinuous
UniformSpace.toTopologicalSpace
DFunLike.coe
AddMonoidHom
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
AddCommGroup.toAddGroup
instFunLike		completion
add
AddCommGroup.toAddCommMonoid
Continuous.add
AddCommMagma.toAdd
AddCommSemigroup.toAddCommMagma
AddCommMonoid.toAddCommSemigroup
IsTopologicalAddGroup.toContinuousAdd
IsUniformAddGroup.to_topologicalAddGroup
AddCommMonoid.toAddMonoid
UniformSpace.Completion
UniformSpace.Completion.instAddMonoid
UniformSpace.Completion.instAddCommGroup		β€”Continuous.add
IsTopologicalAddGroup.toContinuousAdd
IsUniformAddGroup.to_topologicalAddGroup
ext
UniformSpace.Completion.induction_on
isClosed_eq
T25Space.t2Space
T3Space.t25Space
instT3Space
UniformSpace.Completion.t0Space
UniformSpace.to_regularSpace
continuous_completion
UniformSpace.Completion.isUniformAddGroup
completion_coe
UniformSpace.Completion.coe_add
completion_coe πŸ“–mathematicalContinuous
UniformSpace.toTopologicalSpace
DFunLike.coe
AddMonoidHom
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
instFunLike		UniformSpace.Completion
UniformSpace.Completion.instAddMonoid
completion
UniformSpace.Completion.coe'		β€”UniformSpace.Completion.map_coe
uniformContinuous_addMonoidHom_of_continuous
instAddMonoidHomClass
completion_zero πŸ“–mathematicalβ€”completion
AddMonoidHom
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
instZeroAddMonoidHom
continuous_const
UniformSpace.toTopologicalSpace
UniformSpace.Completion
UniformSpace.Completion.instAddMonoid		β€”ext
continuous_const
UniformSpace.Completion.induction_on
isClosed_eq
T25Space.t2Space
T3Space.t25Space
instT3Space
UniformSpace.Completion.t0Space
UniformSpace.to_regularSpace
continuous_completion
completion_coe
continuous_completion πŸ“–mathematicalContinuous
UniformSpace.toTopologicalSpace
DFunLike.coe
AddMonoidHom
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
instFunLike		UniformSpace.Completion
UniformSpace.Completion.uniformSpace
UniformSpace.Completion.instAddMonoid
completion		β€”UniformSpace.Completion.continuous_map
continuous_extension πŸ“–mathematicalContinuous
UniformSpace.toTopologicalSpace
DFunLike.coe
AddMonoidHom
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
instFunLike		UniformSpace.Completion
UniformSpace.Completion.uniformSpace
UniformSpace.Completion.instAddMonoid
extension		β€”UniformSpace.Completion.continuous_extension
extension_coe πŸ“–mathematicalContinuous
UniformSpace.toTopologicalSpace
DFunLike.coe
AddMonoidHom
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
instFunLike		UniformSpace.Completion
UniformSpace.Completion.instAddMonoid
extension
UniformSpace.Completion.coe'		β€”UniformSpace.Completion.extension_coe
uniformContinuous_addMonoidHom_of_continuous
instAddMonoidHomClass

UniformSpace.Completion

Definitions

NameCategoryTheorems
addGroup πŸ“–CompOp
3 mathmath: PositiveLinearMap.gnsStarAlgHom_apply, isUniformAddGroup, instNonarchimedeanAddGroupCompletion
instAddCommGroup πŸ“–CompOp
11 mathmath: PositiveLinearMap.gnsNonUnitalStarAlgHom_apply_coe, AddMonoidHom.completion_add, PositiveLinearMap.gnsStarAlgHom_apply, Summable.toCompl_tsum, ContinuousLinearMap.completion_apply_coe, ContinuousLinearMap.toAddMonoidHom_completion, summable_iff_cauchySeq_finset_and_tsum_mem, summable_iff_summable_compl_and_tsum_mem, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply, hasSum_iff_hasSum_compl, ContinuousLinearMap.coe_completion
instAddMonoid πŸ“–CompOp
13 mathmath: AddMonoidHom.completion_coe, AddMonoidHom.extension_coe, AddMonoidHom.continuous_completion, AddMonoidHom.completion_add, Summable.toCompl_tsum, AddMonoidHom.continuous_extension, summable_iff_cauchySeq_finset_and_tsum_mem, continuous_toCompl, summable_iff_summable_compl_and_tsum_mem, isDenseInducing_toCompl, toCompl_apply, AddMonoidHom.completion_zero, hasSum_iff_hasSum_compl
instDistribMulActionOfUniformContinuousConstSMul πŸ“–CompOp
3 mathmath: PositiveLinearMap.gnsNonUnitalStarAlgHom_apply_coe, PositiveLinearMap.gnsStarAlgHom_apply, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply
instModule πŸ“–CompOp
9 mathmath: PositiveLinearMap.gnsNonUnitalStarAlgHom_apply_coe, norm_toComplL, PositiveLinearMap.gnsStarAlgHom_apply, coe_toComplβ‚—α΅’, ContinuousLinearMap.completion_apply_coe, ContinuousLinearMap.toAddMonoidHom_completion, coe_toComplL, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply, ContinuousLinearMap.coe_completion
instMulActionWithZeroOfUniformContinuousConstSMul πŸ“–CompOpβ€”
instSubNegMonoid πŸ“–CompOpβ€”
toCompl πŸ“–CompOp
7 mathmath: Summable.toCompl_tsum, summable_iff_cauchySeq_finset_and_tsum_mem, continuous_toCompl, summable_iff_summable_compl_and_tsum_mem, isDenseInducing_toCompl, toCompl_apply, hasSum_iff_hasSum_compl

Theorems

NameKindAssumesProvesValidatesDepends On
coe_add πŸ“–mathematicalβ€”coe'
AddSemigroup.toAdd
AddMonoid.toAddSemigroup
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
UniformSpace.Completion
instAddCompletion		β€”mapβ‚‚_coe_coe
uniformContinuous_add
coe_eq_zero_iff πŸ“–mathematicalβ€”coe'
UniformSpace.Completion
instZeroCompletion		β€”β€”
coe_neg πŸ“–mathematicalβ€”coe'
NegZeroClass.toNeg
SubNegZeroMonoid.toNegZeroClass
SubtractionMonoid.toSubNegZeroMonoid
AddGroup.toSubtractionMonoid
UniformSpace.Completion
instNegCompletion		β€”map_coe
uniformContinuous_neg
coe_sub πŸ“–mathematicalβ€”coe'
SubNegMonoid.toSub
AddGroup.toSubNegMonoid
UniformSpace.Completion
instSubCompletion		β€”mapβ‚‚_coe_coe
uniformContinuous_sub
coe_zero πŸ“–mathematicalβ€”coe'
UniformSpace.Completion
instZeroCompletion		β€”β€”
continuous_toCompl πŸ“–mathematicalβ€”Continuous
UniformSpace.Completion
UniformSpace.toTopologicalSpace
uniformSpace
DFunLike.coe
AddMonoidHom
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
instAddMonoid
AddMonoidHom.instFunLike
toCompl		β€”continuous_coe
isDenseInducing_toCompl πŸ“–mathematicalβ€”IsDenseInducing
UniformSpace.Completion
UniformSpace.toTopologicalSpace
uniformSpace
DFunLike.coe
AddMonoidHom
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
instAddMonoid
AddMonoidHom.instFunLike
toCompl		β€”isDenseInducing_coe
isUniformAddGroup πŸ“–mathematicalβ€”IsUniformAddGroup
UniformSpace.Completion
uniformSpace
addGroup		β€”uniformContinuous_mapβ‚‚
toCompl_apply πŸ“–mathematicalβ€”DFunLike.coe
AddMonoidHom
UniformSpace.Completion
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
instAddMonoid
AddMonoidHom.instFunLike
toCompl
coe'		β€”β€”

(root)

Definitions

NameCategoryTheorems
instAddCompletion πŸ“–CompOp
14 mathmath: LaurentSeries.LaurentSeriesRingEquiv_def, PadicComplex.isNonarchimedean, LaurentSeries.coe_X_compare, LaurentSeries.exists_powerSeries_of_memIntegers, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, LaurentSeries.powerSeriesRingEquiv_coe_apply, Padic.coe_withValRingEquiv, UniformSpace.Completion.mapRingEquiv_apply, Padic.coe_withValRingEquiv_symm, LaurentSeries.ratfuncAdicComplRingEquiv_apply, UniformSpace.Completion.mapRingEquiv_symm_apply, LaurentSeries.mem_integers_of_powerSeries, UniformSpace.Completion.coe_add
instNegCompletion πŸ“–CompOp
1 mathmath: UniformSpace.Completion.coe_neg
instSubCompletion πŸ“–CompOp
1 mathmath: UniformSpace.Completion.coe_sub
instZeroCompletion πŸ“–CompOp
5 mathmath: Valued.extension_eq_zero_iff, UniformSpace.Completion.coe_eq_zero_iff, UniformSpace.Completion.coe_zero, PadicComplex.coe_zero, UniformSpace.Completion.instIsBoundedSMul

---

← Back to Index