Commit 2023-03-06 15:43 306e54f8

View on Github →

feat: port Topology.Algebra.GroupCompletion (#2637)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/GroupCompletion.lean

added def AddMonoidHom.completion

added theorem AddMonoidHom.completion_add

added theorem AddMonoidHom.completion_coe

added theorem AddMonoidHom.completion_zero

added theorem AddMonoidHom.continuous_completion

added theorem AddMonoidHom.continuous_extension

added def AddMonoidHom.extension

added theorem AddMonoidHom.extension_coe

added theorem UniformSpace.Completion.coe_add

added theorem UniformSpace.Completion.coe_neg

added theorem UniformSpace.Completion.coe_sub

added theorem UniformSpace.Completion.coe_zero

added theorem UniformSpace.Completion.continuous_toCompl

added theorem UniformSpace.Completion.denseInducing_toCompl

added def UniformSpace.Completion.toCompl

Modified Mathlib/Topology/UniformSpace/Completion.lean

added def UniformSpace.Completion.coe'