adjointAux_inner_left — Mathlib

English

The inner product of adjointAux A applied to y with x equals the inner product of y with A x.

Русский

Внутреннее произведение (adjointAux A) y по x равно внутреннему произведению y по A x.

LaTeX

$$$$ \\langle \\mathrm{adjointAux} A \\; y, x \\rangle = \\langle y, A x \\rangle. $$$$

Lean4

theorem adjointAux_inner_left (A : E →L[𝕜] F) (x : E) (y : F) : ⟪adjointAux A y, x⟫ = ⟪y, A x⟫ := by
  rw [adjointAux_apply, toDual_symm_apply, toSesqForm_apply_coe, coe_comp', innerSL_apply_coe, Function.comp_apply]

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