inner_toCLM_conjTranspose_left — Mathlib

English

The inner product with toCLM Mᴴ and v against w equals the inner product of v with toCLM M applied to w.

Русский

Плотность скалярного произведения: ⟪toCLM Mᴴ v, w⟫ = ⟪v, toCLM M w⟫.

LaTeX

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

Lean4

theorem inner_toCLM_conjTranspose_left {M : CStarMatrix m n A} {v : C⋆ᵐᵒᵈ(A, n → A)} {w : C⋆ᵐᵒᵈ(A, m → A)} :
    ⟪toCLM Mᴴ v, w⟫_A = ⟪v, toCLM M w⟫_A :=
  by
  simp only [toCLM_apply_eq_sum, pi_inner, equiv_symm_pi_apply, inner_def, Finset.mul_sum, Matrix.conjTranspose_apply,
    star_sum, star_mul, star_star, Finset.sum_mul]
  rw [Finset.sum_comm]
  simp_rw [mul_assoc]

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