adjointAux_inner_right — Mathlib

English

The adjoint of the composition equals the composition of adjoints in reverse order: (A ∘ B)† = B† ∘ A†.

Русский

Сопряжённый композиции равен композиции сопряжённых в обратном порядке: (A ∘ B)† = B† ∘ A†.

LaTeX

$$$$ (A \\circ B)^{\\dagger} = B^{\\dagger} \\circ A^{\\dagger}. $$$$

Lean4

theorem adjointAux_inner_right (A : E →L[𝕜] F) (x : E) (y : F) : ⟪x, adjointAux A y⟫ = ⟪A x, y⟫ := by
  rw [← inner_conj_symm, adjointAux_inner_left, inner_conj_symm]

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