Theorem Submodule.toLinearMap_subtypeL

Modification history

2026-05-20 20:03
Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean
chore: split Topology.Algebra.Module.LinearMap (#39612) …
Modified Submodule.toLinearMap_subtypeLView on Github →
2026-05-10 22:27
Mathlib/Topology/Algebra/Module/LinearMap.lean
refactor(Topology/Algebra/Module/LinearMap): rename subtypeL companion lemmas (#38962) …
Added Submodule.toLinearMap_subtypeLView on Github →