Commit 2023-05-18 09:10 8126cf11

View on Github →

feat: port Analysis.NormedSpace.Completion (#4072)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/Completion.lean

added theorem UniformSpace.Completion.coe_toComplL

added theorem UniformSpace.Completion.coe_toComplₗᵢ

added theorem UniformSpace.Completion.norm_toComplL

added def UniformSpace.Completion.toComplL

added def UniformSpace.Completion.toComplₗᵢ

Modified Mathlib/Topology/Algebra/GroupCompletion.lean

Modified Mathlib/Topology/MetricSpace/Completion.lean