isStarProjection_iff' — Mathlib

English

An element p is a star projection in a ring with star if and only if p is idempotent and self-adjoint, i.e., p^2 = p and p^* = p.

Русский

Элемент p является звездной проекцией в кольце с операцией сопряжения тогда и только тогда, когда p идемпотентен и самосопряжён, то есть p^2 = p и p^* = p.

LaTeX

$$$ \text{IsStarProjection}(p) \iff (p^2 = p \land p^* = p). $$$

Lean4

theorem _root_.isStarProjection_iff' [Mul R] [Star R] : IsStarProjection p ↔ p * p = p ∧ star p = p :=
  isStarProjection_iff _

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