Projection

📁 Source: Mathlib/Analysis/CStarAlgebra/Projection.lean

Statistics

Metric	Count
Definitions	0
Theorems isSelfAdjoint_iff_isStarNormal, isStarProjection_iff_isIdempotentElem_and_isStarNormal	2
Total	2

IsIdempotentElem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSelfAdjoint_iff_isStarNormal 📖	mathematical	IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid IsStarNormal	—	Complex.instNontrivial IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar quasispectrum_subset Set.mem_singleton_iff

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isStarProjection_iff_isIdempotentElem_and_isStarNormal 📖	mathematical	—	IsStarProjection Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid IsIdempotentElem IsStarNormal	—	Complex.instNontrivial IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar IsIdempotentElem.isSelfAdjoint_iff_isStarNormal isStarProjection_iff

---

← Back to Index