adjoint_adjoint — Mathlib

English

The adjoint operation is an involution on the space of linear maps; applying it twice returns the original map.

Русский

Операция сопряжённого равна двойному применению: возвращает исходную карту.

LaTeX

$$$(A^{*})^{*} = A$$$

Lean4

/-- The adjoint is involutive. -/
@[simp]
theorem adjoint_adjoint (A : E →ₗ[𝕜] F) : A.adjoint.adjoint = A :=
  by
  ext v
  refine ext_inner_left 𝕜 fun w => ?_
  rw [adjoint_inner_right, adjoint_inner_left]

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