Commit 2025-04-23 16:05 2ae18410

View on Github →

refactor: generalise ContinuousLinearMap.restrictScalars to semirings (#24232) The motivation here is to restrict scalars from R to R≥0, which happens when considering pointed cones as submodules. Also rename the pair M, M₂ to M₁, M₂ for consistency. From Toric

Estimated changes

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

modified theorem ContinuousLinearMap.coe_restrictScalars'

modified theorem ContinuousLinearMap.coe_restrictScalars

modified theorem ContinuousLinearMap.coe_restrictScalarsₗ

modified def ContinuousLinearMap.restrictScalars

modified theorem ContinuousLinearMap.restrictScalars_add

modified theorem ContinuousLinearMap.restrictScalars_neg

modified theorem ContinuousLinearMap.restrictScalars_smul

added theorem ContinuousLinearMap.restrictScalars_sub

modified theorem ContinuousLinearMap.restrictScalars_zero

modified def ContinuousLinearMap.restrictScalarsₗ

modified theorem ContinuousLinearMap.toContinuousAddMonoidHom_restrictScalars