chore(LinearMap/Defs): misc minor clean-up

Mathlib/Algebra/Module/Equiv/Defs.lean

@@ -171,9 +171,11 @@ instance : SemilinearEquivClass (M ≃ₛₗ[σ] M₂) σ M M₂ where
   map_add := (·.map_add')
   map_smulₛₗ := (·.map_smul')
 
-theorem toLinearMap_eq_coe {e : M ≃ₛₗ[σ] M₂} : e.toLinearMap = SemilinearMapClass.semilinearMap e :=
+theorem toLinearMap_eq_ofClass {e : M ≃ₛₗ[σ] M₂} : e.toLinearMap = SemilinearMap.ofClass e :=
   rfl
 
+@[deprecated (since := "2026-09-03")] alias toLinearMap_eq_coe := toLinearMap_eq_ofClass
+
 @[simp]
 theorem coe_mk {f invFun left_inv right_inv} :
     ((⟨f, invFun, left_inv, right_inv⟩ : M ≃ₛₗ[σ] M₂) : M → M₂) = f := rfl

Mathlib/Algebra/Module/LinearMap/Defs.lean

@@ -156,31 +156,40 @@ variable {F} (f : F) [FunLike F M M₃] [SemilinearMapClass F σ M M₃]
 theorem map_smul_inv {σ' : S →+* R} [RingHomInvPair σ σ'] (c : S) (x : M) :
     c • f x = f (σ' c • x) := by simp [map_smulₛₗ _]
 
-/-- Reinterpret an element of a type of semilinear maps as a semilinear map. -/
+/-- Reinterpret an element of a type of semilinear maps as a semilinear map.
+
+See `LinearMap.ofClass` for the analogous definition on *linear* maps.
+(In the linear case, both coincide.) -/
 @[coe]
-def semilinearMap : M →ₛₗ[σ] M₃ where
+def _root_.SemilinearMap.ofClass : M →ₛₗ[σ] M₃ where
   toFun := f
   map_add' := map_add f
   map_smul' := map_smulₛₗ f
 
 /-- Reinterpret an element of a type of semilinear maps as a semilinear map. -/
 instance instCoeToSemilinearMap : CoeHead F (M →ₛₗ[σ] M₃) where
-  coe f := semilinearMap f
+  coe f := SemilinearMap.ofClass f
 
 end SemilinearMapClass
 
+@[deprecated (since := "2026-09-03")] alias SemilinearMapClass.semilinearMap :=
+  SemilinearMap.ofClass
+
 namespace LinearMapClass
 variable {F : Type*} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂]
   (f : F) [FunLike F M₁ M₂] [LinearMapClass F R M₁ M₂]
 
-/-- Reinterpret an element of a type of linear maps as a linear map. -/
-abbrev _root_.LinearMap.ofClass : M₁ →ₗ[R] M₂ := SemilinearMapClass.semilinearMap f
+/-- Reinterpret an element of a type of linear maps as a linear map.
+See `SemilinearMap.ofClass` for the analogous definition on *semilinear* maps.
+(In the linear case, both coincide.)
+-/
+abbrev _root_.LinearMap.ofClass : M₁ →ₗ[R] M₂ := SemilinearMap.ofClass f
 
 @[deprecated (since := "2026-09-03")] alias linearMap := LinearMap.ofClass
 
 /-- Reinterpret an element of a type of linear maps as a linear map. -/
 instance instCoeToLinearMap : CoeHead F (M₁ →ₗ[R] M₂) where
-  coe f := SemilinearMapClass.semilinearMap f
+  coe f := SemilinearMap.ofClass f
 
 end LinearMapClass
 
@@ -209,10 +218,12 @@ instance semilinearMapClass : SemilinearMapClass (M →ₛₗ[σ] M₃) σ M M
   map_add f := f.map_add'
   map_smulₛₗ := LinearMap.map_smul'
 
+-- TODO: should this be renamed to `SemilinearMap.coe_ofClass`?
 @[simp, norm_cast]
-lemma coe_coe {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] {f : F} :
-    ⇑(f : M →ₛₗ[σ] M₃) = f :=
+lemma coe_ofClass {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] {f : F} :
+    ⇑(SemilinearMap.ofClass f) = f :=
   rfl
+@[deprecated (since := "2026-09-07")] alias coe_coe := coe_ofClass
 
 /-- The `DistribMulActionHom` underlying a `LinearMap`. -/
 def toDistribMulActionHom (f : M →ₛₗ[σ] M₃) : DistribMulActionHom σ.toMonoidHom M M₃ :=
@@ -255,15 +266,18 @@ theorem coe_addHom_mk {σ : R →+* S} (f : AddHom M M₃) (h) :
   rfl
 
 theorem coe_semilinearMap {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] (f : F) :
-    ((f : M →ₛₗ[σ] M₃) : M → M₃) = f :=
+    ⇑(SemilinearMap.ofClass f) = f :=
   rfl
+-- TODO: is duplicate to coe_ofClass!
+--@[deprecated (since := "2026-09-07")] alias coe_semilinearMap := coe_semilinearMap
 
-theorem toLinearMap_injective {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃]
-    {f g : F} (h : (f : M →ₛₗ[σ] M₃) = (g : M →ₛₗ[σ] M₃)) :
+theorem ofClass_injective {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃]
+    {f g : F} (h : SemilinearMap.ofClass f = SemilinearMap.ofClass g) :
     f = g := by
   apply DFunLike.ext
   intro m
   exact DFunLike.congr_fun h m
+@[deprecated (since := "2026-09-07")] alias toLinearMap_injective := ofClass_injective
 
 /-- Identity map as a `LinearMap` -/
 @[instance_reducible]
@@ -274,7 +288,7 @@ theorem id_apply (x : M) : @id R M _ _ _ x = x :=
   rfl
 
 @[simp, norm_cast]
-theorem id_coe : ((LinearMap.id : M →ₗ[R] M) : M → M) = _root_.id :=
+theorem id_coe : ⇑((LinearMap.id : M →ₗ[R] M)) = _root_.id :=
   rfl
 
 /-- A generalisation of `LinearMap.id` that constructs the identity function
@@ -289,7 +303,7 @@ def id' {σ : R →+* R} [RingHomId σ] : M →ₛₗ[σ] M where
     rfl
 
 @[simp, norm_cast]
-theorem id'_coe {σ : R →+* R} [RingHomId σ] : ((id' : M →ₛₗ[σ] M) : M → M) = _root_.id :=
+theorem id'_coe {σ : R →+* R} [RingHomId σ] : ⇑(id' : M →ₛₗ[σ] M) = _root_.id :=
   rfl
 
 end

Mathlib/RepresentationTheory/Intertwining.lean

@@ -74,8 +74,10 @@ instance : LinearMapClass (IntertwiningMap ρ σ) A V W where
 -- we are actively moving away from these design decisions.
 -- See e.g. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Concrete.20homomorphism.20type.20vs.20abstract.20class/with/492579416
 @[simp]
-lemma coe_eq_toLinearMap {f : IntertwiningMap ρ σ} :
-  SemilinearMapClass.semilinearMap f = f.toLinearMap := rfl
+lemma ofClass_eq_toLinearMap {f : IntertwiningMap ρ σ} :
+  SemilinearMap.ofClass f = f.toLinearMap := rfl
+
+@[deprecated (since := "2026-09-03")] alias coe_eq_toLinearMap := ofClass_eq_toLinearMap
 
 @[simp] theorem coe_mk (f : V →ₗ[A] W) (h) : ⇑(⟨f, h⟩ : IntertwiningMap ρ σ) = f := rfl
 

Mathlib/RingTheory/Bialgebra/Convolution.lean

@@ -113,7 +113,7 @@ lemma convOne_apply (c : C) : (1 : WithConv <| C →ₐc[R] A) c = algebraMap R
 
 @[simp]
 lemma toLinearMap_convOne :
-    toConv (SemilinearMapClass.semilinearMap (1 : WithConv <| C →ₐc[R] A).ofConv) = 1 := rfl
+    toConv (SemilinearMap.ofClass (1 : WithConv <| C →ₐc[R] A).ofConv) = 1 := rfl
 
 @[simp] lemma toAlgHom_convOne : toConv (1 : WithConv <| C →ₐc[R] A).ofConv.toAlgHom = 1 := rfl
 
@@ -131,7 +131,7 @@ lemma convMul_def (f g : WithConv <| C →ₐc[R] A) :
 
 private lemma convPow_succ (f : WithConv <| C →ₐc[R] A) (n : ℕ) : f ^ (n + 1) = (f ^ n) * f := rfl
 
--- TODO: Make simp once `SemilinearMapClass.semilinearMap` is not simp nf anymore.
+-- TODO: Make simp once `SemilinearMap.ofClass` is not simp nf anymore.
 -- @[simp]
 lemma toLinearMap_convMul (f g : WithConv <| C →ₐc[R] A) :
     toConv (f * g).ofConv.toLinearMap = toConv f.ofConv.toLinearMap * toConv g.ofConv.toLinearMap :=
@@ -142,7 +142,7 @@ lemma toAlgHom_convMul (f g : WithConv <| C →ₐc[R] A) :
     toConv (f * g).ofConv.toAlgHom = toConv f.ofConv.toAlgHom * toConv g.ofConv.toAlgHom :=
   rfl
 
--- TODO: Make simp once `SemilinearMapClass.semilinearMap` is not simp nf anymore.
+-- TODO: Make simp once `SemilinearMap.ofClass` is not simp nf anymore.
 -- @[simp]
 lemma toLinearMap_convPow (f : WithConv <| C →ₐc[R] A) :
     ∀ n, toConv (f ^ n).ofConv.toLinearMap = toConv f.ofConv.toLinearMap ^ n

Mathlib/RingTheory/Finiteness/Basic.lean

@@ -265,7 +265,7 @@ instance quotient (R) {A M} [Semiring R] [AddCommGroup M] [Ring A] [Module A M]
 
 /-- The range of a linear map from a finite module is finite. -/
 instance range [Module.Finite R M] (f : M →ₗ[R] N) : Module.Finite R f.range :=
-  of_surjective (SemilinearMapClass.semilinearMap f).rangeRestrict
+  of_surjective f.rangeRestrict
     fun ⟨_, y, hy⟩ => ⟨y, Subtype.ext hy⟩
 
 /-- Pushforwards of finite submodules are finite. -/