Commit 2026-08-12 18:02 2015830c

View on Github →

chore(Topology/Algebra/LinearMapCompletion): generalize UniformSpace.Completion.toComplL (#41740) Generalize and move toComplL to a more appropriate file.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Reproducing.lean

Modified Mathlib/Analysis/Normed/Module/Completion.lean

deleted theorem UniformSpace.Completion.coe_toComplL

deleted def UniformSpace.Completion.toComplL

added theorem UniformSpace.Completion.toContinuousLinearMap_toComplₗᵢ

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral/DistLEIntegral.lean

Modified Mathlib/Topology/Algebra/LinearMapCompletion.lean

added theorem UniformSpace.Completion.coe_toComplL

added theorem UniformSpace.Completion.toAddMonoidHom_toComplL

added def UniformSpace.Completion.toComplL