Def UniformSpace.Completion.toComplL

Modification history

2023-05-18 09:10

Mathlib/Analysis/NormedSpace/Completion.lean

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

Added UniformSpace.Completion.toComplL View on Github →