Theorem Submodule.toLinearMap_mkQL

Modification history

2026-05-20 20:03

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

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

Modified Submodule.toLinearMap_mkQL View 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.toLinearMap_mkQL View on Github →