Theorem UniformSpace.Completion.toContinuousLinearMap_toComplₗᵢ

Modification history

2026-08-12 18:02
Mathlib/Analysis/Normed/Module/Completion.lean
chore(Topology/Algebra/LinearMapCompletion): generalize `UniformSpace.Completion.toComplL` (#41740) …
Added UniformSpace.Completion.toContinuousLinearMap_toComplₗᵢView on Github →