English
For c ∈ R and M, (c • M)^H = star c • M^H.
Русский
Для скаляра c из кольца R и матрицы M: (c • M)^H = star c • M^H.
LaTeX
$$$ (c \cdot M)^{H} = \overline{c} \cdot M^{H} $$$
Lean4
/-- Note that `StarModule` is quite a strong requirement; as such we also provide the following
variants which this lemma would not apply to:
* `Matrix.conjTranspose_smul_non_comm`
* `Matrix.conjTranspose_nsmul`
* `Matrix.conjTranspose_zsmul`
* `Matrix.conjTranspose_natCast_smul`
* `Matrix.conjTranspose_intCast_smul`
* `Matrix.conjTranspose_inv_natCast_smul`
* `Matrix.conjTranspose_inv_intCast_smul`
* `Matrix.conjTranspose_ratCast_smul`
-/
@[simp]
theorem conjTranspose_smul [Star R] [Star α] [SMul R α] [StarModule R α] (c : R) (M : Matrix m n α) :
(c • M)ᴴ = star c • Mᴴ :=
Matrix.ext fun _ _ => star_smul _ _
