Commit 2026-05-10 22:27 090daf0b
View on Github →refactor(Topology/Algebra/Module/LinearMap): rename subtypeL companion lemmas (#38962)
This PR renames the companion lemmas of Submodule.subtypeL for consistency with Submodule.mkQL (introduced in PR #38811). Specifically, Submodule.coe_subtypeL is renamed to Submodule.toLinearMap_subtypeL (to accurately reflect that it projects to the underlying LinearMap, not a function-level coercion), and Submodule.coe_subtypeL' is renamed to Submodule.coe_subtypeL (since this is the genuine function-level coercion lemma).