conjTranspose_inv_natCast_smul — Mathlib

English

Let R be a division semiring and α an additive commutative monoid with a star; for c ∈ ℕ, the conjugate transpose commutes with the inverse scalar: ((c : R)⁻¹ • M)^H = (c : R)⁻¹ • M^H.

Русский

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

LaTeX

$$$ ((c : R)^{-1} \cdot M)^H = (c : R)^{-1} \cdot M^H $$$

Lean4

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

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