Theorem Submodule.toLinearMap_liftQL

Modification history

2026-05-20 20:03
Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean
chore: split Topology.Algebra.Module.LinearMap (#39612) …
Modified Submodule.toLinearMap_liftQLView on Github →
2026-05-12 22:40
Mathlib/Topology/Algebra/Module/LinearMap.lean
feat: continuous version of Submodule.liftQ (#39273)
Added Submodule.toLinearMap_liftQLView on Github →