isStarProjection_iff_isSymmetricProjection

English

A star projection is equivalent to being a symmetric projection on a Hilbert space, i.e., the projection equals its own adjoint under certain representations.

Русский

Звёздная проекция эквивалентна симметричной проекции на гильбертовом пространстве в заданной форме.

LaTeX

$$$\\text{IsStarProjection}(T) \\iff T.\\IsSymmetricProjection$$$

Lean4

theorem isStarProjection_iff_isSymmetricProjection : IsStarProjection T ↔ T.IsSymmetricProjection := by
  simp [isStarProjection_iff, LinearMap.isSymmetricProjection_iff, isSelfAdjoint_iff_isSymmetric, IsIdempotentElem,
    End.mul_eq_comp, ← coe_comp, mul_def]

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