Theorem Submodule.coe_mkQL

Modification history

2026-05-20 20:03
Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean
chore: split Topology.Algebra.Module.LinearMap (#39612) …
Modified Submodule.coe_mkQLView on Github →
2026-05-04 13:04
Mathlib/Topology/Algebra/Module/LinearMap.lean
feat(Topology/Algebra/Module): bundle Submodule.mkQ as a continuous linear map (#38811) …
Added Submodule.coe_mkQLView on Github →