feat(algebra/algebra/basic,data/matrix/basic): resolve a TODO about alg_hom.map_smul_of_tower (#12684)

It turns out that this lemma doesn't actually help in the place I claimed it would, so I added the lemma that does help too.

Author: eric-wieser

src/algebra/algebra/basic.lean

@@ -670,6 +670,10 @@ by { ext, refl }
   of_linear_map linear_map.id map_one map_mul = alg_hom.id R A :=
 ext $ λ _, rfl
 
+lemma map_smul_of_tower {R'} [has_scalar R' A] [has_scalar R' B]
+  [linear_map.compatible_smul A B R' R] (r : R') (x : A) : φ (r • x) = r • φ x :=
+φ.to_linear_map.map_smul_of_tower r x
+
 lemma map_list_prod (s : list A) :
   φ s.prod = (s.map φ).prod :=
 φ.to_ring_hom.map_list_prod s

src/data/matrix/basic.lean

@@ -151,6 +151,20 @@ lemma map_smul [has_scalar R α] [has_scalar R β] (f : α → β) (r : R)
   (hf : ∀ a, f (r • a) = r • f a) (M : matrix m n α) : (r • M).map f = r • (M.map f) :=
 ext $ λ _ _, hf _
 
+/-- The scalar action via `has_mul.to_has_scalar` is transformed by the same map as the elements
+of the matrix, when `f` preserves multiplication. -/
+lemma map_smul' [has_mul α] [has_mul β] (f : α → β) (r : α) (A : matrix n n α)
+  (hf : ∀ a₁ a₂, f (a₁ * a₂) = f a₁ * f a₂) :
+  (r • A).map f = f r • A.map f :=
+ext $ λ _ _, hf _ _
+
+/-- The scalar action via `has_mul.to_has_opposite_scalar` is transformed by the same map as the
+elements of the matrix, when `f` preserves multiplication. -/
+lemma map_op_smul' [has_mul α] [has_mul β] (f : α → β) (r : α) (A : matrix n n α)
+  (hf : ∀ a₁ a₂, f (a₁ * a₂) = f a₁ * f a₂) :
+  (mul_opposite.op r • A).map f = mul_opposite.op (f r) • A.map f :=
+ext $ λ _ _, hf _ _
+
 lemma _root_.is_smul_regular.matrix [has_scalar R S] {k : R} (hk : is_smul_regular S k) :
   is_smul_regular (matrix m n S) k :=
 is_smul_regular.pi $ λ _, is_smul_regular.pi $ λ _, hk

src/linear_algebra/matrix/adjugate.lean

@@ -438,11 +438,8 @@ begin
   let A' := mv_polynomial_X n n ℤ,
   suffices : adjugate (adjugate A') = det A' ^ (fintype.card n - 2) • A',
   { rw [←mv_polynomial_X_map_matrix_aeval ℤ A, ←alg_hom.map_adjugate, ←alg_hom.map_adjugate, this,
-      ←alg_hom.map_det, ← alg_hom.map_pow],
-    -- TODO: missing an `alg_hom.map_smul_of_tower` here.
-    ext i j,
-    dsimp [-mv_polynomial_X],
-    rw [←alg_hom.map_mul] },
+      ←alg_hom.map_det, ← alg_hom.map_pow, alg_hom.map_matrix_apply, alg_hom.map_matrix_apply,
+      matrix.map_smul' _ _ _ (_root_.map_mul _)] },
   have h_card' : fintype.card n - 2 + 1 = fintype.card n - 1,
   { simp [h_card] },