Theorem Submodule.coe_liftQL

Modification history

2026-05-20 20:03

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

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

Modified Submodule.coe_liftQL View on Github →

2026-05-12 22:40

Mathlib/Topology/Algebra/Module/LinearMap.lean

feat: continuous version of Submodule.liftQ (#39273)

Added Submodule.coe_liftQL View on Github →