refactor(Topology/Algebra/Module/LinearMap): rename subtypeL companion lemmas (leanprover-community#38962)

This PR renames the companion lemmas of `Submodule.subtypeL` for consistency with `Submodule.mkQL` (introduced in PR leanprover-community#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).

Author: sharky564

Mathlib/Analysis/Calculus/Implicit.lean

@@ -428,11 +428,11 @@ theorem to_implicitFunctionOfComplemented (hf : HasStrictFDerivAt f f' a) (hf' :
   swap
   · ext
     simp only [Classical.choose_spec hker, implicitFunctionDataOfComplemented,
-      ContinuousLinearMap.comp_apply, Submodule.coe_subtypeL', Submodule.coe_subtype,
+      ContinuousLinearMap.comp_apply, Submodule.coe_subtypeL, Submodule.coe_subtype,
       ContinuousLinearMap.id_apply]
   swap
   · ext
-    simp only [ContinuousLinearMap.comp_apply, Submodule.coe_subtypeL', Submodule.coe_subtype,
+    simp only [ContinuousLinearMap.comp_apply, Submodule.coe_subtypeL, Submodule.coe_subtype,
       ContinuousLinearMap.apply_val_ker, ContinuousLinearMap.zero_apply]
   simp only [implicitFunctionDataOfComplemented, map_sub, sub_self]
 

Mathlib/Analysis/Normed/Operator/Banach.lean

@@ -498,10 +498,9 @@ noncomputable def coprodSubtypeLEquivOfIsCompl {F : Type*} [NormedAddCommGroup F
   ContinuousLinearEquiv.ofBijective (f.coprod G.subtypeL)
     (by
       rw [ker_coprod_of_disjoint_range]
-      · rw [hker, Submodule.ker_subtypeL, Submodule.prod_bot]
-      · rw [Submodule.range_subtypeL]
-        exact h.disjoint)
-    (by simp only [range_coprod, Submodule.range_subtypeL, h.sup_eq_top])
+      · simp [hker]
+      · simp [h.disjoint])
+    (by simp [LinearMap.range_coprod, h.sup_eq_top])
 
 theorem range_eq_map_coprodSubtypeLEquivOfIsCompl {F : Type*} [NormedAddCommGroup F]
     [NormedSpace 𝕜 F] [CompleteSpace F] (f : E →L[𝕜] F) {G : Submodule 𝕜 F}

Mathlib/Topology/Algebra/Module/LinearMap.lean

@@ -702,31 +702,6 @@ theorem coe_rangeRestrict [RingHomSurjective σ₁₂] (f : M₁ →SL[σ₁₂]
       (f : M₁ →ₛₗ[σ₁₂] M₂).rangeRestrict :=
   rfl
 
-/-- `Submodule.subtype` as a `ContinuousLinearMap`. -/
-def _root_.Submodule.subtypeL (p : Submodule R₁ M₁) : p →L[R₁] M₁ where
-  cont := continuous_subtype_val
-  toLinearMap := p.subtype
-
-@[simp, norm_cast]
-theorem _root_.Submodule.coe_subtypeL (p : Submodule R₁ M₁) :
-    (p.subtypeL : p →ₗ[R₁] M₁) = p.subtype :=
-  rfl
-
-@[simp]
-theorem _root_.Submodule.coe_subtypeL' (p : Submodule R₁ M₁) : ⇑p.subtypeL = p.subtype :=
-  rfl
-
-@[simp]
-theorem _root_.Submodule.subtypeL_apply (p : Submodule R₁ M₁) (x : p) : p.subtypeL x = x :=
-  rfl
-
-theorem _root_.Submodule.range_subtypeL (p : Submodule R₁ M₁) :
-    range (p.subtypeL : p →ₗ[R₁] M₁) = p :=
-  Submodule.range_subtype _
-
-theorem _root_.Submodule.ker_subtypeL (p : Submodule R₁ M₁) : ker (p.subtypeL : p →ₗ[R₁] M₁) = ⊥ :=
-  Submodule.ker_subtype _
-
 section
 
 variable {R S : Type*} [Semiring R] [Semiring S] [Module R M₁] [Module R M₂] [Module R S]
@@ -1258,6 +1233,37 @@ end ContinuousLinearMap
 
 namespace Submodule
 
+section Semiring
+
+variable {R : Type*} [Semiring R] {M : Type*} [TopologicalSpace M] [AddCommMonoid M] [Module R M]
+
+/-- `Submodule.subtype` as a `ContinuousLinearMap`. -/
+def subtypeL (p : Submodule R M) : p →L[R] M where
+  toLinearMap := p.subtype
+
+@[simp, norm_cast]
+theorem toLinearMap_subtypeL (p : Submodule R M) : (p.subtypeL : p →ₗ[R] M) = p.subtype := rfl
+
+@[simp]
+theorem coe_subtypeL (p : Submodule R M) : ⇑p.subtypeL = p.subtype := rfl
+
+@[deprecated (since := "2026-05-06")]
+alias coe_subtypeL' := coe_subtypeL
+
+theorem subtypeL_apply (p : Submodule R M) (x : p) : p.subtypeL x = x := by simp
+
+@[deprecated range_subtype (since := "2026-05-06")]
+theorem range_subtypeL (p : Submodule R M) : (p.subtypeL : p →ₗ[R] M).range = p :=
+  Submodule.range_subtype _
+
+@[deprecated ker_subtype (since := "2026-05-06")]
+theorem ker_subtypeL (p : Submodule R M) : (p.subtypeL : p →ₗ[R] M).ker = ⊥ :=
+  Submodule.ker_subtype _
+
+end Semiring
+
+section Ring
+
 variable {R : Type*} [Ring R] {M : Type*} [TopologicalSpace M] [AddCommGroup M] [Module R M]
   (S : Submodule R M)
 
@@ -1281,6 +1287,8 @@ theorem isQuotientMap_mkQL : IsQuotientMap S.mkQL := isQuotientMap_quot_mk
 theorem isOpenQuotientMap_mkQL [ContinuousAdd M] : IsOpenQuotientMap S.mkQL :=
   S.isOpenQuotientMap_mkQ
 
+end Ring
+
 end Submodule
 
 namespace ContinuousLinearMap

scripts/nolints_prime_decls.txt

@@ -4144,7 +4144,6 @@ Sublattice.coe_inf'
 SubmoduleClass.module'
 Submodule.coe_continuous_linearProjOfClosedCompl'
 Submodule.coe_prodEquivOfIsCompl'
-Submodule.coe_subtypeL'
 Submodule.comap_smul'
 Submodule.disjoint_def'
 Submodule.disjoint_span_singleton'