inner_toCLM_conjTranspose_right — Mathlib

English

Symmetric statement to the left version: ⟪v, toCLM Mᴴ w⟫ = ⟪toCLM M v, w⟫.

Русский

Симметричное утверждение: ⟪v, toCLM Mᴴ w⟫ = ⟪toCLM M v, w⟫.

LaTeX

$$$\langle v, toCLM M^H w \rangle_A = \langle toCLM M v, w \rangle_A$$$

Lean4

theorem inner_toCLM_conjTranspose_right {M : CStarMatrix m n A} {v : C⋆ᵐᵒᵈ(A, m → A)} {w : C⋆ᵐᵒᵈ(A, n → A)} :
    ⟪v, toCLM Mᴴ w⟫_A = ⟪toCLM M v, w⟫_A := by
  apply Eq.symm
  simpa using inner_toCLM_conjTranspose_left (M := Mᴴ) (v := v) (w := w)

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