Theorem ContinuousLinearMap.restrictScalars_sub

Modification history

2026-05-20 20:03

Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean

chore: split Topology.Algebra.Module.LinearMap (#39612) …

Modified ContinuousLinearMap.restrictScalars_sub View on Github →

2025-04-23 16:05

Mathlib/Topology/Algebra/Module/LinearMap.lean

refactor: generalise `ContinuousLinearMap.restrictScalars` to semirings (#24232) …

Added ContinuousLinearMap.restrictScalars_sub View on Github →