conjTranspose_smul_non_comm — Mathlib

English

If the scalar action is compatible with star in a specified way, then (c • M)^H = star c • M^H.

Русский

Если действие скаляра совместимо со звездой в заданном виде, то (c • M)^H = star c • M^H.

LaTeX

$$$ (c \cdot M)^{H} = \overline{c} \cdot M^{H} \quad \text{under suitable compatibility} $$$

Lean4

@[simp]
theorem conjTranspose_smul_non_comm [Star R] [Star α] [SMul R α] [SMul Rᵐᵒᵖ α] (c : R) (M : Matrix m n α)
    (h : ∀ (r : R) (a : α), star (r • a) = MulOpposite.op (star r) • star a) :
    (c • M)ᴴ = MulOpposite.op (star c) • Mᴴ :=
  Matrix.ext <| by simp [h]

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