conjTranspose_intCast_smul — Mathlib

English

Let R be a ring and α an additive commutative monoid with a star, and M a matrix over α. For any integer c, the conjugate transpose commutes with the scalar (c : R) • M: ((c : R) • M)^H = (c : R) • M^H.

Русский

Пусть R — кольцо, α — аддитивный коммутативный моноид со звездой, и M — матрица над α. Для любого целого 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_intCast_smul [Ring R] [AddCommGroup α] [StarAddMonoid α] [Module R α] (c : ℤ) (M : Matrix m n α) :
    ((c : R) • M)ᴴ = (c : R) • Mᴴ :=
  Matrix.ext <| by simp

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