conjTranspose_inv_intCast_smul — Mathlib

English

Let c ∈ ℤ, R a division ring, α AddCommGroup with a Star, and M a matrix. Then ((c : R)⁻¹ • M)^H = (c : R)⁻¹ • M^H.

Русский

Пусть c ∈ ℤ и R — кольцо деления; α — добавочная группа с единичной трансформацией, M — матрица. Тогда ((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_intCast_smul [DivisionRing R] [AddCommGroup α] [StarAddMonoid α] [Module R α] (c : ℤ)
    (M : Matrix m n α) : ((c : R)⁻¹ • M)ᴴ = (c : R)⁻¹ • Mᴴ :=
  Matrix.ext <| by simp

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