[Merged by Bors] - chore: rename SemilinearMapClass.semilinearMap to LinearMap.ofClass

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 = .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

@@ -158,31 +158,20 @@ theorem map_smul_inv {σ' : S →+* R} [RingHomInvPair σ σ'] (c : S) (x : M) :
 
 /-- Reinterpret an element of a type of semilinear maps as a semilinear map. -/
 @[coe]
-def semilinearMap : M →ₛₗ[σ] M₃ where
+def _root_.LinearMap.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 := LinearMap.ofClass f
 
 end SemilinearMapClass
 
-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
-
-@[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
-
-end LinearMapClass
+@[deprecated (since := "2026-09-03")] alias SemilinearMapClass.semilinearMap :=
+  LinearMap.ofClass
+@[deprecated (since := "2026-09-03")] alias LinearMapClass.linearMap := LinearMap.ofClass
 
 namespace LinearMap
 
@@ -210,10 +199,12 @@ instance semilinearMapClass : SemilinearMapClass (M →ₛₗ[σ] M₃) σ M M
   map_smulₛₗ := LinearMap.map_smul'
 
 @[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} :
+    ⇑(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₃ :=
   { f with map_zero' := show f 0 = 0 from map_zero f }
@@ -254,17 +245,16 @@ theorem coe_addHom_mk {σ : R →+* S} (f : AddHom M M₃) (h) :
     ((LinearMap.mk f h : M →ₛₗ[σ] M₃) : AddHom M M₃) = f :=
   rfl
 
-theorem coe_semilinearMap {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] (f : F) :
-    ((f : M →ₛₗ[σ] M₃) : M → M₃) = f :=
-  rfl
+@[deprecated (since := "2026-09-07")] alias coe_semilinearMap := coe_ofClass
 
-theorem toLinearMap_injective {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃]
-    {f g : F} (h : (f : M →ₛₗ[σ] M₃) = (g : M →ₛₗ[σ] M₃)) :
-    f = g := by
+theorem ofClass_injective {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃]
+    {f g : F} (h : ofClass f = 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]
 def id : M →ₗ[R] M :=

Mathlib/Algebra/Module/Submodule/EqLocus.lean

@@ -78,7 +78,7 @@ include τ₁₂ in
 theorem eqOn_sup {f g : F} {S T : Submodule R M}
     (hS : Set.EqOn f g S) (hT : Set.EqOn f g T) :
     Set.EqOn f g ↑(S ⊔ T) := by
-  rw [← LinearMap.coe_coe (f := f), ← LinearMap.coe_coe (f := g), ← le_eqLocus] at hS hT ⊢
+  rw [← LinearMap.coe_ofClass (f := f), ← LinearMap.coe_ofClass (f := g), ← le_eqLocus] at hS hT ⊢
   exact sup_le hS hT
 
 include τ₁₂ in

Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean

@@ -453,7 +453,7 @@ def mapₙₐ [Fintype n] [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A
   map_mul' M N := by
     ext
     -- Un-squeezing this `simp` seems to add about half a second elaboration time.
-    simp only [mapₗ_apply, map, LinearMap.coe_coe, ofMatrix_apply, mul_apply, map_sum, map_mul,
+    simp only [mapₗ_apply, map, LinearMap.coe_ofClass, ofMatrix_apply, mul_apply, map_sum, map_mul,
       ofMatrix_apply]
   map_star' M := by ext; simp [map, star_apply, map_star]
 

Mathlib/Analysis/CStarAlgebra/CompletelyPositiveMap.lean

@@ -133,7 +133,7 @@ lemma map_cstarMatrix_nonneg {n : Type*} [Fintype n] (φ : A₁ →CP A₂) (M :
   let k := Fintype.card n
   let e := Fintype.equivFinOfCardEq (rfl : Fintype.card n = k)
   have hmain : 0 ≤ (reindexₐ ℂ A₁ e M).mapₗ (φ : A₁ →ₗ[ℂ] A₂) := by
-    simp only [mapₗ, LinearMap.coe_coe, LinearMap.coe_mk, AddHom.coe_mk]
+    simp only [mapₗ, LinearMap.coe_ofClass, LinearMap.coe_mk, AddHom.coe_mk]
     exact CompletelyPositiveMapClass.map_cstarMatrix_nonneg' _ k _ (map_nonneg _ hM)
   rw [← mapₗ_reindexₐ] at hmain
   simpa [reindexₐ_symm] using map_nonneg (reindexₐ ℂ A₂ e).symm hmain

Mathlib/Analysis/Matrix/HermitianFunctionalCalculus.lean

@@ -76,7 +76,7 @@ lemma isClosedEmbedding_cfcAux : IsClosedEmbedding hA.cfcAux := by
   have h2 :
       diagonal (RCLike.ofReal ∘ f ∘ fun i ↦ ⟨hA.eigenvalues i, hA.eigenvalues_mem_spectrum_real i⟩)
         = (0 : Matrix n n 𝕜) := by
-    simp only [LinearMap.coe_coe, cfcAux_apply, conjStarAlgAut_apply] at hf
+    simp only [LinearMap.coe_ofClass, cfcAux_apply, conjStarAlgAut_apply] at hf
     replace hf := congr($hf * (hA.eigenvectorUnitary : Matrix n n 𝕜))
     simp only [mul_assoc, SetLike.coe_mem, Unitary.star_mul_self_of_mem, mul_one, zero_mul] at hf
     simpa [← mul_assoc] using congr((star hA.eigenvectorUnitary : Matrix n n 𝕜) * $hf)

Mathlib/Analysis/Normed/Operator/Basic.lean

@@ -66,7 +66,7 @@ theorem ball_zero_subset_range_iff_surjective [RingHomSurjective σ₁₂] {f :
 theorem ball_subset_range_iff_surjective [RingHomSurjective σ₁₂] {f : 𝓕} {x : F} {r : ℝ}
     (hr : 0 < r) : ball x r ⊆ Set.range f ↔ (⇑f).Surjective := by
   refine ⟨fun h ↦ ?_, by simp_all⟩
-  rw [← ball_zero_subset_range_iff_surjective hr, ← LinearMap.coe_coe]
+  rw [← ball_zero_subset_range_iff_surjective hr, ← LinearMap.coe_ofClass]
   simp_rw [← LinearMap.coe_range, Set.subset_def, SetLike.mem_coe] at h ⊢
   intro _ _
   rw [← Submodule.add_mem_iff_left (f : E →ₛₗ[σ₁₂] F).range (h _ <| mem_ball_self hr)]

Mathlib/LinearAlgebra/AffineSpace/Homogenization.lean

@@ -171,7 +171,7 @@ section
 variable {F : Type*} [FunLike F (Homogenization R P) W] [LinearMapClass F R _ _]
 
 theorem hom_ext {f g : F} (h : ∀ x, f (ofPoint x) = g (ofPoint x)) : f = g := by
-  apply LinearMap.toLinearMap_injective
+  apply LinearMap.ofClass_injective
   rwa [← LinearMap.eqLocus_eq_top, eq_top_iff, ← span_range_ofPoint, Submodule.span_le,
     Set.range_subset_iff]
 

Mathlib/LinearAlgebra/TensorProduct/Submodule.lean

@@ -73,7 +73,7 @@ theorem mulMap_map_comp_eq {T : Type w} [Semiring T] [Algebra R T] (f : S →ₐ
   ext
   simp only [TensorProduct.AlgebraTensorModule.curry_apply,
     TensorProduct.curry_apply, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
-    Function.comp_apply, TensorProduct.map_tmul, mulMap_tmul, LinearMap.coe_coe, map_mul]
+    Function.comp_apply, TensorProduct.map_tmul, mulMap_tmul, LinearMap.coe_ofClass, map_mul]
   rfl
 
 theorem coe_mulMap_comp_eq {T : Type w} [Semiring T] [Algebra R T] (f : S →ₐ[R] T) :

Mathlib/RepresentationTheory/Intertwining.lean

@@ -74,8 +74,9 @@ 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 ρ σ} : .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/RepresentationTheory/Rep/Res.lean

@@ -31,7 +31,7 @@ namespace Rep
 @[expose, implicit_reducible]
 def resMap {X Y : Rep k G} (f : H →* G) (p : X ⟶ Y) :
     of (X := X.V) (X.ρ.comp f) ⟶ of (X := Y.V) (Y.ρ.comp f) :=
-  ofHom ⟨p.hom, fun h ↦ by simpa using p.hom.2 (f h)⟩
+  ofHom ⟨p.hom, fun h ↦ by simpa using! p.hom.2 (f h)⟩
 
 /-- The restriction functor `Rep R G ⥤ Rep R H` for a subgroup `H` of `G`. -/
 abbrev resFunctor (f : H →* G) : Rep.{t} k G ⥤ Rep k H where

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 (LinearMap.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 `LinearMap.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 `LinearMap.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/Coalgebra/Basic.lean

@@ -143,15 +143,15 @@ theorem sum_counit_tmul_map_eq {B : Type*} [AddCommMonoid B] [Module R B]
     ∑ i ∈ repr.index, counit (R := R) (repr.left i) ⊗ₜ f (repr.right i) = 1 ⊗ₜ[R] f a := by
   have := sum_counit_tmul_eq repr
   apply_fun LinearMap.lTensor R (f : A →ₗ[R] B) at this
-  simp_all only [map_sum, LinearMap.lTensor_tmul, LinearMap.coe_coe]
+  simp_all only [map_sum, LinearMap.lTensor_tmul, LinearMap.coe_ofClass]
 
 @[simp]
 theorem sum_map_tmul_counit_eq {B : Type*} [AddCommMonoid B] [Module R B]
     {F : Type*} [FunLike F A B] [LinearMapClass F R A B] (f : F) (a : A) {repr : Repr R a ι} :
     ∑ i ∈ repr.index, f (repr.left i) ⊗ₜ counit (R := R) (repr.right i) = f a ⊗ₜ[R] 1 := by
   have := sum_tmul_counit_eq repr
   apply_fun LinearMap.rTensor R (f : A →ₗ[R] B) at this
-  simp_all only [map_sum, LinearMap.rTensor_tmul, LinearMap.coe_coe]
+  simp_all only [map_sum, LinearMap.rTensor_tmul, LinearMap.coe_ofClass]
 
 -- Cannot be @[simp] because `a₁` cannot be inferred by `simp`.
 theorem sum_map_tmul_tmul_eq {B : Type*} [AddCommMonoid B] [Module R B]
@@ -164,7 +164,7 @@ theorem sum_map_tmul_tmul_eq {B : Type*} [AddCommMonoid B] [Module R B]
   have := sum_tmul_tmul_eq repr a₁ a₂
   apply_fun TensorProduct.map (f : A →ₗ[R] B)
     (TensorProduct.map (g : A →ₗ[R] B) (h : A →ₗ[R] B)) at this
-  simp_all only [map_sum, TensorProduct.map_tmul, LinearMap.coe_coe]
+  simp_all only [map_sum, TensorProduct.map_tmul, LinearMap.coe_ofClass]
 
 lemma sum_counit_smul (𝓡 : Repr R a ι) :
     ∑ x ∈ 𝓡.index, counit (R := R) (𝓡.left x) • 𝓡.right x = a := by

Mathlib/RingTheory/Coalgebra/Equiv.lean

@@ -313,7 +313,7 @@ structure on `B`. -/
     ext x
     simpa only [toCoalgHom_eq_coe, CoalgHom.toLinearMap_eq_coe, LinearMap.coe_comp,
       LinearEquiv.coe_coe, Function.comp_apply, ← (ℛ R _).eq, map_sum, TensorProduct.map_tmul,
-      LinearMap.coe_coe, CoalgHom.coe_coe, LinearMap.rTensor_tmul, coe_symm_toLinearEquiv,
+      LinearMap.coe_ofClass, CoalgHom.coe_coe, LinearMap.rTensor_tmul, coe_symm_toLinearEquiv,
       symm_apply_apply, LinearMap.lTensor_comp_map, TensorProduct.sum_tmul,
       TensorProduct.assoc_tmul, TensorProduct.tmul_sum] using (sum_map_tmul_tmul_eq f f f x).symm
   rTensor_counit_comp_comul := by

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. -/

Mathlib/RingTheory/LocalRing/Quotient.lean

@@ -38,7 +38,7 @@ theorem quotient_span_eq_top_iff_span_eq_top (s : Set S) :
   have H : (span (R ⧸ p) ((Ideal.Quotient.mk (I := pS)) '' s)).restrictScalars R =
       (span R s).map (IsScalarTower.toAlgHom R S (S ⧸ pS) : S →ₗ[R] S ⧸ pS) := by
     rw [map_span, ← restrictScalars_span R (R ⧸ p) Ideal.Quotient.mk_surjective,
-      LinearMap.coe_coe, IsScalarTower.coe_toAlgHom', Ideal.Quotient.algebraMap_eq]
+      LinearMap.coe_ofClass, IsScalarTower.coe_toAlgHom', Ideal.Quotient.algebraMap_eq]
   constructor
   · intro hs
     rw [← top_le_iff]
@@ -55,7 +55,7 @@ theorem quotient_span_eq_top_iff_span_eq_top (s : Set S) :
   · intro hs
     rwa [hs, Submodule.map_top, LinearMap.range_eq_top.mpr,
       restrictScalars_eq_top_iff] at H
-    rw [LinearMap.coe_coe, IsScalarTower.coe_toAlgHom', Ideal.Quotient.algebraMap_eq]
+    rw [LinearMap.coe_ofClass, IsScalarTower.coe_toAlgHom', Ideal.Quotient.algebraMap_eq]
     exact Ideal.Quotient.mk_surjective
 
 attribute [local instance] Ideal.Quotient.field