conjTranspose_rat_smul — Mathlib

English

Let α be an additive group with a star and a ℚ-module structure. For c ∈ ℚ and M a matrix with entries in α, (c • M)^H = c • M^H.

Русский

Пусть α — аддитивная группа со звездой и есть структура модуля над ℚ. Для c ∈ ℚ и матрицы M: (c • M)^H = c • M^H.

LaTeX

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

Lean4

theorem conjTranspose_rat_smul [AddCommGroup α] [StarAddMonoid α] [Module ℚ α] (c : ℚ) (M : Matrix m n α) :
    (c • M)ᴴ = c • Mᴴ :=
  Matrix.ext <| by simp

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