Commit 2026-05-20 20:03 2b7518f9

View on Github →

chore: split Topology.Algebra.Module.LinearMap (#39612) We could definitely split a bit more, but I think that's a good start

Estimated changes

deleted theorem Submodule.coe_liftQL
deleted theorem Submodule.coe_mkQL
deleted theorem Submodule.coe_subtypeL
deleted theorem Submodule.ker_subtypeL
deleted def Submodule.liftQL
deleted theorem Submodule.liftQL_apply
deleted def Submodule.mkQL
deleted theorem Submodule.mkQL_apply
deleted theorem Submodule.range_subtypeL
deleted def Submodule.subtypeL
deleted theorem Submodule.subtypeL_apply
added theorem Submodule.coe_liftQL
added theorem Submodule.coe_mkQL
added def Submodule.liftQL
added theorem Submodule.liftQL_apply
added def Submodule.mkQL
added theorem Submodule.mkQL_apply
added theorem Submodule.coe_subtypeL
added theorem Submodule.ker_subtypeL