Commit 2025-06-28 23:20 47db34f3

View on Github →

feat(Algebra/Star/StarProjection): define star projections (#26052) This pr defines star projections, which are self-adjoint idempotents. In star-ordered rings, they are non-negative. (this was discussed in #25958)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Idempotent.lean

added theorem IsIdempotentElem.pow_eq

Modified Mathlib/Algebra/Order/Star/Basic.lean

added theorem IsStarProjection.le_one

added theorem IsStarProjection.mem_Icc

added theorem IsStarProjection.nonneg

added theorem IsStarProjection.one_sub_nonneg

Modified Mathlib/Algebra/Ring/Idempotent.lean

added theorem IsIdempotentElem.add

added theorem IsIdempotentElem.commute_of_anticommute

added theorem IsIdempotentElem.mul_eq_zero_of_anticommute

added theorem isIdempotentElem_iff_mul_one_sub_self

added theorem isIdempotentElem_iff_one_sub_mul_self

Modified Mathlib/Algebra/Star/SelfAdjoint.lean

modified theorem IsSelfAdjoint.isStarNormal

Created Mathlib/Algebra/Star/StarProjection.lean

added theorem IsStarProjection.add

added theorem IsStarProjection.add_sub_mul_of_commute

added theorem IsStarProjection.isStarNormal

added theorem IsStarProjection.mul

added theorem IsStarProjection.mul_one_sub_self

added theorem IsStarProjection.one_sub

added theorem IsStarProjection.one_sub_mul_self

added theorem IsStarProjection.pow_eq

added theorem IsStarProjection.pow_succ_eq

added structure IsStarProjection

added theorem isStarProjection_iff'

added theorem isStarProjection_one_sub_iff

Modified Mathlib/Algebra/Star/Unitary.lean

added theorem IsStarProjection.two_mul_sub_one_mem_unitary