chore: drop redundant LinearMap/LinearEquiv.map_sum (#7426)

Note that `_root_.map_sum` is not marked as `@[simp]`.
leanprover-community · Oct 2, 2023 · 89ef311 · 89ef311
1 parent f1a26d7
commit 89ef311
Show file tree

Hide file tree

Showing 6 changed files with 7 additions and 13 deletions.
diff --git a/Mathlib/LinearAlgebra/Alternating/Basic.lean b/Mathlib/LinearAlgebra/Alternating/Basic.lean
@@ -954,7 +954,7 @@ theorem compMultilinearMap_alternatization (g : N' →ₗ[R] N'₂)
     MultilinearMap.alternatization (g.compMultilinearMap f)
       = g.compAlternatingMap (MultilinearMap.alternatization f) := by
   ext
-  simp [MultilinearMap.alternatization_def]
+  simp [MultilinearMap.alternatization_def, map_sum]
 #align linear_map.comp_multilinear_map_alternatization LinearMap.compMultilinearMap_alternatization
 
 end LinearMap

diff --git a/Mathlib/LinearAlgebra/Basic.lean b/Mathlib/LinearAlgebra/Basic.lean
@@ -168,10 +168,7 @@ variable [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₂
 variable [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄]
 variable (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃)
 
-@[simp]
-theorem map_sum {ι : Type*} {t : Finset ι} {g : ι → M} : f (∑ i in t, g i) = ∑ i in t, f (g i) :=
-  f.toAddMonoidHom.map_sum _ _
-#align linear_map.map_sum LinearMap.map_sum
+#align linear_map.map_sum map_sumₓ
 
 
 /-- The restriction of a linear map `f : M → M₂` to a submodule `p ⊆ M` gives a linear map
@@ -1759,10 +1756,7 @@ variable {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPai
 
 variable (e e' : M ≃ₛₗ[σ₁₂] M₂)
 
-@[simp]
-theorem map_sum {s : Finset ι} (u : ι → M) : e (∑ i in s, u i) = ∑ i in s, e (u i) :=
-  e.toLinearMap.map_sum
-#align linear_equiv.map_sum LinearEquiv.map_sum
+#align linear_equiv.map_sum map_sumₓ
 
 theorem map_eq_comap {p : Submodule R M} :
     (p.map (e : M →ₛₗ[σ₁₂] M₂) : Submodule R₂ M₂) = p.comap (e.symm : M₂ →ₛₗ[σ₂₁] M) :=

diff --git a/Mathlib/LinearAlgebra/Basis.lean b/Mathlib/LinearAlgebra/Basis.lean
@@ -158,7 +158,7 @@ theorem repr_symm_apply (v) : b.repr.symm v = Finsupp.total ι M R b v :=
   calc
     b.repr.symm v = b.repr.symm (v.sum Finsupp.single) := by simp
     _ = ∑ i in v.support, b.repr.symm (Finsupp.single i (v i)) :=
-      by rw [Finsupp.sum, LinearEquiv.map_sum]
+      by rw [Finsupp.sum, map_sum]
     _ = Finsupp.total ι M R b v := by simp [repr_symm_single, Finsupp.total_apply, Finsupp.sum]
 #align basis.repr_symm_apply Basis.repr_symm_apply
 

diff --git a/Mathlib/LinearAlgebra/Matrix/Adjugate.lean b/Mathlib/LinearAlgebra/Matrix/Adjugate.lean
@@ -277,7 +277,7 @@ theorem cramer_eq_adjugate_mulVec (A : Matrix n n α) (b : n → α) :
   conv_lhs =>
     rw [this]
   ext k
-  simp [mulVec, dotProduct, mul_comm]
+  simp [mulVec, dotProduct, mul_comm, map_sum]
 #align matrix.cramer_eq_adjugate_mul_vec Matrix.cramer_eq_adjugate_mulVec
 
 theorem mul_adjugate_apply (A : Matrix n n α) (i j k) :

diff --git a/Mathlib/LinearAlgebra/Pi.lean b/Mathlib/LinearAlgebra/Pi.lean
@@ -149,7 +149,7 @@ def lsum (S) [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] [Semir
     simp [apply_single]
   right_inv f := by
     ext x
-    suffices f (∑ j, Pi.single j (x j)) = f x by simpa [apply_single]
+    suffices f (∑ j, Pi.single j (x j)) = f x by simpa [apply_single, map_sum]
     rw [Finset.univ_sum_single]
 #align linear_map.lsum LinearMap.lsum
 #align linear_map.lsum_symm_apply LinearMap.lsum_symm_apply

diff --git a/Mathlib/NumberTheory/ClassNumber/Finite.lean b/Mathlib/NumberTheory/ClassNumber/Finite.lean
@@ -99,7 +99,7 @@ theorem norm_le (a : S) {y : ℤ} (hy : ∀ k, abv (bS.repr a k) ≤ y) :
   --   exact finset.mem_image.mpr ⟨⟨i, j, k⟩, Finset.mem_univ _, rfl⟩
   rw [← LinearMap.det_toMatrix bS]
   convert Matrix.det_sum_smul_le (n := ι) Finset.univ _ hy using 3
-  · simp; rfl
+  · simp [map_sum]; rfl
   · rw [Finset.card_univ, smul_mul_assoc, mul_comm]
   · intro i j k
     apply Finset.le_max'