conjTranspose_natCast_smul — Mathlib

English

Let R be a semiring and α an additive commutative monoid with a star. For every natural number c, the conjugate transpose commutes with scalar multiplication by c in R: ((c : R) • M)^H = (c : R) • M^H.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem conjTranspose_natCast_smul [Semiring R] [AddCommMonoid α] [StarAddMonoid α] [Module R α] (c : ℕ)
    (M : Matrix m n α) : ((c : R) • M)ᴴ = (c : R) • Mᴴ :=
  Matrix.ext <| by simp

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