feat(data/matrix/basic): even more lemmas about conj_transpose and smul (#13970)

It turns out none of the lemmas in the previous #13938 were the ones I needed.

Author: eric-wieser

src/algebra/star/module.lean

@@ -13,6 +13,8 @@ import linear_algebra.prod
 We define `star_linear_equiv`, which is the star operation bundled as a star-linear map.
 It is defined on a star algebra `A` over the base ring `R`.
 
+This file also provides some lemmas that need `algebra.module.basic` imported to prove.
+
 ## TODO
 
 - Define `star_linear_equiv` for noncommutative `R`. We only the commutative case for now since,
@@ -25,10 +27,35 @@ It is defined on a star algebra `A` over the base ring `R`.
   equivalence.
 -/
 
+section smul_lemmas
+variables {R M : Type*}
+
+@[simp] lemma star_int_cast_smul [ring R] [add_comm_group M] [module R M] [star_add_monoid M]
+  (n : ℤ) (x : M) : star ((n : R) • x) = (n : R) • star x :=
+map_int_cast_smul (star_add_equiv : M ≃+ M) R R n x
+
+@[simp] lemma star_nat_cast_smul [semiring R] [add_comm_monoid M] [module R M] [star_add_monoid M]
+  (n : ℕ) (x : M) : star ((n : R) • x) = (n : R) • star x :=
+map_nat_cast_smul (star_add_equiv : M ≃+ M) R R n x
+
+@[simp] lemma star_inv_int_cast_smul [division_ring R] [add_comm_group M] [module R M]
+  [star_add_monoid M] (n : ℤ) (x : M) : star ((n⁻¹ : R) • x) = (n⁻¹ : R) • star x :=
+map_inv_int_cast_smul (star_add_equiv : M ≃+ M) R R n x
+
+@[simp] lemma star_inv_nat_cast_smul [division_ring R] [add_comm_group M] [module R M]
+  [star_add_monoid M] (n : ℕ) (x : M) : star ((n⁻¹ : R) • x) = (n⁻¹ : R) • star x :=
+map_inv_nat_cast_smul (star_add_equiv : M ≃+ M) R R n x
+
+@[simp] lemma star_rat_cast_smul [division_ring R] [add_comm_group M] [module R M]
+  [star_add_monoid M] (n : ℚ) (x : M) : star ((n : R) • x) = (n : R) • star x :=
+map_rat_cast_smul (star_add_equiv : M ≃+ M) _ _ _ x
+
 @[simp] lemma star_rat_smul {R : Type*} [add_comm_group R] [star_add_monoid R] [module ℚ R]
   (x : R) (n : ℚ) : star (n • x) = n • star x :=
 map_rat_smul (star_add_equiv : R ≃+ R) _ _
 
+end smul_lemmas
+
 /-- If `A` is a module over a commutative `R` with compatible actions,
 then `star` is a semilinear equivalence. -/
 @[simps]

src/data/matrix/basic.lean

@@ -1340,7 +1340,12 @@ variants which this lemma would not apply to:
 * `matrix.conj_transpose_smul_non_comm`
 * `matrix.conj_transpose_nsmul`
 * `matrix.conj_transpose_zsmul`
+* `matrix.conj_transpose_nat_cast_smul`
+* `matrix.conj_transpose_int_cast_smul`
+* `matrix.conj_transpose_inv_nat_cast_smul`
+* `matrix.conj_transpose_inv_int_cast_smul`
 * `matrix.conj_transpose_rat_smul`
+* `matrix.conj_transpose_rat_cast_smul`
 -/
 @[simp] lemma conj_transpose_smul [has_star R] [has_star α] [has_scalar R α] [star_module R α]
   (c : R) (M : matrix m n α) :
@@ -1365,6 +1370,26 @@ matrix.ext $ by simp
   (c • M)ᴴ = c • Mᴴ :=
 matrix.ext $ by simp
 
+@[simp] lemma conj_transpose_nat_cast_smul [semiring R] [add_comm_monoid α]
+  [star_add_monoid α] [module R α] (c : ℕ) (M : matrix m n α) : ((c : R) • M)ᴴ = (c : R) • Mᴴ :=
+matrix.ext $ by simp
+
+@[simp] lemma conj_transpose_int_cast_smul [ring R] [add_comm_group α]
+  [star_add_monoid α] [module R α] (c : ℤ) (M : matrix m n α) : ((c : R) • M)ᴴ = (c : R) • Mᴴ :=
+matrix.ext $ by simp
+
+@[simp] lemma conj_transpose_inv_nat_cast_smul [division_ring R] [add_comm_group α]
+  [star_add_monoid α] [module R α] (c : ℕ) (M : matrix m n α) : ((c : R)⁻¹ • M)ᴴ = (c : R)⁻¹ • Mᴴ :=
+matrix.ext $ by simp
+
+@[simp] lemma conj_transpose_inv_int_cast_smul [division_ring R] [add_comm_group α]
+  [star_add_monoid α] [module R α] (c : ℤ) (M : matrix m n α) : ((c : R)⁻¹ • M)ᴴ = (c : R)⁻¹ • Mᴴ :=
+matrix.ext $ by simp
+
+@[simp] lemma conj_transpose_rat_cast_smul [division_ring R] [add_comm_group α] [star_add_monoid α]
+  [module R α] (c : ℚ) (M : matrix m n α) : ((c : R) • M)ᴴ = (c : R) • Mᴴ :=
+matrix.ext $ by simp
+
 @[simp] lemma conj_transpose_rat_smul [add_comm_group α] [star_add_monoid α] [module ℚ α] (c : ℚ)
   (M : matrix m n α) : (c • M)ᴴ = c • Mᴴ :=
 matrix.ext $ by simp