isSymmetric_iff_isSelfAdjoint — Mathlib

English

For a basis b of E, A = B† iff ∀ i y, ⟪A(b_i), y⟫ = ⟪b_i, B y⟫.

Русский

Для базиса b пространства E, A = B† тогда и только тогда, когда ∀ i y выполняется ⟪A(b_i), y⟫ = ⟪b_i, B y⟫.

LaTeX

$$$$A = B^{*} \iff \forall i,y, \langle A(b_i), y\rangle = \langle b_i, B y\rangle.$$$$

Lean4

theorem isSymmetric_iff_isSelfAdjoint (A : E →ₗ[𝕜] E) : IsSymmetric A ↔ IsSelfAdjoint A :=
  by
  rw [isSelfAdjoint_iff', IsSymmetric, ← LinearMap.eq_adjoint_iff]
  exact eq_comm

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