Commit 2025-09-22 13:30 eb83b6d6
View on Github →chore(Analysis/Normed/Completeness): Generalize extend to uniform groups (#29869)
Since the continuous linear maps are defined for topological vector spaces, we can generalize ContinuousLinearMap.extend
so that the dense subspace is not a normed space anymore.