conjTranspose_zsmul — Mathlib

English

Let α be an additive group with a star operation, and M a matrix with entries in α. For any integer c, the conjugate transpose commutes with scalar multiplication: (c • M)^H = c • M^H.

Русский

Пусть α — аддитивная группа с операцией сопряжения, и M — матрица над α. Для любого целого числа c сопряжённое транспонирование коммутирует скалярное умножение: (c • M)^H = c • M^H.

LaTeX

$$$ (c \cdot M)^H = c \cdot M^H $$$

Lean4

@[simp]
theorem conjTranspose_zsmul [AddGroup α] [StarAddMonoid α] (c : ℤ) (M : Matrix m n α) : (c • M)ᴴ = c • Mᴴ :=
  Matrix.ext <| by simp

Похожие утверждения