Documentation

Mathlib.Algebra.Star.StarProjection

Star projections #

This file defines star projections, which are self-adjoint idempotents.

In star-ordered rings, star projections are non-negative. (See IsStarProjection.nonneg in Mathlib/Algebra/Order/Star/Basic.lean.)

source
structure IsStarProjection {R : Type u_1} [Mul R] [Star R] (p : R) :
Prop

A star projection is a self-adjoint idempotent.

Instances For
    source
    theorem isStarProjection_iff {R : Type u_1} [Mul R] [Star R] (p : R) :
    IsStarProjection p ↔ IsIdempotentElem p ∧ IsSelfAdjoint p
    source
    theorem isStarProjection_iff' {R : Type u_1} {p : R} [Mul R] [Star R] :
    IsStarProjection p ↔ p * p = p ∧ star p = p
    source
    theorem IsStarProjection.isStarNormal {R : Type u_1} {p : R} [Mul R] [Star R] (hp : IsStarProjection p) :
    IsStarNormal p
    source
    @[simp]
    theorem IsStarProjection.zero (R : Type u_1) [NonUnitalNonAssocSemiring R] [StarAddMonoid R] :
    IsStarProjection 0
    source
    @[simp]
    theorem IsStarProjection.one (R : Type u_1) [MulOneClass R] [StarMul R] :
    IsStarProjection 1
    source
    theorem IsStarProjection.pow_eq {R : Type u_1} {p : R} [Monoid R] [Star R] (hp : IsStarProjection p) {n : ℕ} (hn : n ≠ 0) :
    p ^ n = p
    source
    theorem IsStarProjection.pow_succ_eq {R : Type u_1} {p : R} [Monoid R] [Star R] (hp : IsStarProjection p) (n : ℕ) :
    p ^ (n + 1) = p
    source
    theorem IsStarProjection.one_sub {R : Type u_1} {p : R} [NonAssocRing R] [StarRing R] (hp : IsStarProjection p) :
    IsStarProjection (1 - p)
    source
    theorem isStarProjection_one_sub_iff {R : Type u_1} {p : R} [NonAssocRing R] [StarRing R] :
    IsStarProjection (1 - p) ↔ IsStarProjection p
    source
    theorem IsStarProjection.of_one_sub {R : Type u_1} {p : R} [NonAssocRing R] [StarRing R] :
    IsStarProjection (1 - p) → IsStarProjection p

    Alias of the forward direction of isStarProjection_one_sub_iff.

    source
    theorem IsStarProjection.mul_one_sub_self {R : Type u_1} {p : R} [NonAssocRing R] [Star R] (hp : IsStarProjection p) :
    p * (1 - p) = 0
    source
    theorem IsStarProjection.one_sub_mul_self {R : Type u_1} {p : R} [NonAssocRing R] [Star R] (hp : IsStarProjection p) :
    (1 - p) * p = 0
    source
    theorem IsStarProjection.add {R : Type u_1} {p q : R} [NonUnitalNonAssocSemiring R] [StarRing R] (hp : IsStarProjection p) (hq : IsStarProjection q) (hpq : p * q = 0) :
    IsStarProjection (p + q)

    The sum of star projections is a star projection if their product is 0.

    source
    theorem IsStarProjection.mul {R : Type u_1} {p q : R} [NonUnitalSemiring R] [StarRing R] (hp : IsStarProjection p) (hq : IsStarProjection q) (hpq : Commute p q) :
    IsStarProjection (p * q)

    The product of star projections is a star projection if they commute.

    source
    theorem IsStarProjection.add_sub_mul_of_commute {R : Type u_1} {p q : R} [Ring R] [StarRing R] (hpq : Commute p q) (hp : IsStarProjection p) (hq : IsStarProjection q) :
    IsStarProjection (p + q - p * q)