Commit 2024-08-12 20:23 38dc174b

View on Github →

feat(StrongTopology): generalize ContinuousLinearMap.restrictScalarsL (#15285)

Estimated changes

Modified Mathlib/Algebra/Group/Action/Pi.lean

added theorem Pi.smul_def'

Modified Mathlib/Analysis/LocallyConvex/Bounded.lean

added theorem Bornology.IsVonNBounded.extend_scalars

added theorem Bornology.IsVonNBounded.of_subsingleton

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

deleted theorem ContinuousLinearMap.coe_restrictScalarsL

deleted theorem ContinuousLinearMap.coe_restrict_scalarsL'

deleted def ContinuousLinearMap.restrictScalarsL

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

added theorem ContinuousLinearMap.coe_restrictScalarsL

added theorem ContinuousLinearMap.coe_restrict_scalarsL'

added theorem ContinuousLinearMap.continuous_restrictScalars

added theorem ContinuousLinearMap.embedding_restrictScalars

added def ContinuousLinearMap.restrictScalarsL

added theorem ContinuousLinearMap.uniformContinuous_restrictScalars

added theorem ContinuousLinearMap.uniformEmbedding_restrictScalars

added theorem ContinuousLinearMap.uniformEmbedding_toUniformOnFun

Modified Mathlib/Topology/Bornology/Absorbs.lean