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.

Estimated changes