Commit 2024-09-08 03:59 29aaa179

View on Github →

feat: generalize ContinuousMultilinearMap.restrictScalarsLinear (#16110) ... from normed spaces to topological spaces. Also drop the Fintype assumption.

Estimated changes

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

deleted theorem ContinuousMultilinearMap.continuous_restrictScalars

deleted def ContinuousMultilinearMap.restrictScalarsLinear

Modified Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean

added theorem ContinuousMultilinearMap.continuous_restrictScalars

added theorem ContinuousMultilinearMap.embedding_restrictScalars

added def ContinuousMultilinearMap.restrictScalarsLinear

added theorem ContinuousMultilinearMap.uniformContinuous_restrictScalars

added theorem ContinuousMultilinearMap.uniformEmbedding_restrictScalars