Projection

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

Statistics

Metric	Count
Definitions	0
Theorems isIdempotentElem_iff_quasispectrum_subset, isIdempotentElem_iff_spectrum_subset, isIdempotentElem_star_mul_self_iff_isIdempotentElem_self_mul_star	3
Total	3

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIdempotentElem_iff_quasispectrum_subset 📖	mathematical	—	IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Set Set.instHasSubset quasispectrum Semifield.toCommSemiring Field.toSemifield Set.instInsert MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Set.instSingletonSet AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	EuclideanDomain.toNontrivial IsIdempotentElem.quasispectrum_subset IsIdempotentElem.eq_1 IsLocalRing.toNontrivial Field.instIsLocalRing cfcₙ_id' cfcₙ_mul continuousOn_id' cfcₙ_congr
isIdempotentElem_iff_spectrum_subset 📖	mathematical	—	IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Set Set.instHasSubset spectrum Semifield.toCommSemiring Field.toSemifield Set.instInsert MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Set.instSingletonSet AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	EuclideanDomain.toNontrivial IsScalarTower.right Algebra.to_smulCommClass
isIdempotentElem_star_mul_self_iff_isIdempotentElem_self_mul_star 📖	mathematical	—	IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal EuclideanDomain.toNontrivial isIdempotentElem_iff_quasispectrum_subset quasispectrum.mul_comm

---

← Back to Index