Projection

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

Statistics

Metric	Count
Definitions	0
Theorems isSelfAdjoint_iff_isStarNormal, commute_of_le, le_iff_idempotent_sub, le_iff_mul_eq_left, le_iff_mul_eq_right, le_iff_sub, le_tfae, isStarProjection_iff_isIdempotentElem_and_isStarNormal, isStarProjection_iff_quasispectrum_subset_and_isSelfAdjoint, isStarProjection_iff_quasispectrum_subset_and_isStarNormal, isStarProjection_iff_spectrum_subset_and_isSelfAdjoint, isStarProjection_iff_spectrum_subset_and_isStarNormal	12
Total	12

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 NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	Complex.instNontrivial IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar quasispectrum_subset Set.mem_singleton_iff

IsStarProjection

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commute_of_le 📖	mathematical	IsStarProjection Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalCStarAlgebra.toStarRing Preorder.toLE PartialOrder.toPreorder	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing	—	commute_iff_eq le_iff_mul_eq_right le_iff_mul_eq_left
le_iff_idempotent_sub 📖	mathematical	IsStarProjection Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalCStarAlgebra.toStarRing	Preorder.toLE PartialOrder.toPreorder IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup	—	List.TFAE.out le_tfae
le_iff_mul_eq_left 📖	mathematical	IsStarProjection Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalCStarAlgebra.toStarRing	Preorder.toLE PartialOrder.toPreorder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing	—	List.TFAE.out le_tfae
le_iff_mul_eq_right 📖	mathematical	IsStarProjection Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalCStarAlgebra.toStarRing	Preorder.toLE PartialOrder.toPreorder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing	—	List.TFAE.out le_tfae
le_iff_sub 📖	mathematical	IsStarProjection Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalCStarAlgebra.toStarRing	Preorder.toLE PartialOrder.toPreorder IsStarProjection Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalCStarAlgebra.toStarRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup	—	List.TFAE.out le_tfae
le_tfae 📖	mathematical	IsStarProjection Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalCStarAlgebra.toStarRing	List.TFAE Preorder.toLE PartialOrder.toPreorder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing IsStarProjection InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalCStarAlgebra.toStarRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup IsIdempotentElem	—	mul_sub IsIdempotentElem.eq isIdempotentElem sub_mul le_antisymm NonUnitalCStarAlgebra.toIsScalarTower NonUnitalCStarAlgebra.toSMulCommClass mul_one inr conjugate_le_conjugate_of_nonneg NonUnitalCStarAlgebra.toStarModule Unitization.instStarOrderedRing le_one nonneg Unitization.inr_le_iff LE.le.isSelfAdjoint IsSelfAdjoint.conjugate_nonneg isSelfAdjoint SMulCommClass.complexToReal IsScalarTower.complexToReal IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus Complex.instNontrivial IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar IsStarNormal.instNonUnitalIsometricContinuousFunctionalCalculus CStarAlgebra.instNonnegSpectrumClass' CFC.sqrt_mul_sqrt_self IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsOrderedAddMonoid.toIsOrderedCancelAddMonoid StarOrderedRing.toIsOrderedAddMonoid MulZeroClass.mul_zero norm_eq_zero sq_eq_zero_iff isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass CFC.IsSelfAdjoint.norm_mul_mul_self_of_nonneg NonUnitalCStarAlgebra.toCStarRing StarMul.star_mul IsSelfAdjoint.star_eq sub_of_mul_eq_left IsSelfAdjoint.sub List.tfae_of_cycle

(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
isStarProjection_iff_quasispectrum_subset_and_isSelfAdjoint 📖	mathematical	—	IsStarProjection Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Set Real Set.instHasSubset quasispectrum Real.instCommSemiring Set.instInsert Real.instZero Set.instSingletonSet Real.instOne IsSelfAdjoint	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal isIdempotentElem_iff_quasispectrum_subset isStarProjection_iff
isStarProjection_iff_quasispectrum_subset_and_isStarNormal 📖	mathematical	—	IsStarProjection Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Set Complex Set.instHasSubset quasispectrum Complex.instCommSemiring Set.instInsert Complex.instZero Set.instSingletonSet Complex.instOne IsStarNormal	—	Complex.instNontrivial IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar isIdempotentElem_iff_quasispectrum_subset isStarProjection_iff_isIdempotentElem_and_isStarNormal
isStarProjection_iff_spectrum_subset_and_isSelfAdjoint 📖	mathematical	—	IsStarProjection Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Set Real Set.instHasSubset spectrum Real.instCommSemiring Set.instInsert Real.instZero Set.instSingletonSet Real.instOne IsSelfAdjoint	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal IsScalarTower.right Algebra.to_smulCommClass isIdempotentElem_iff_spectrum_subset isStarProjection_iff
isStarProjection_iff_spectrum_subset_and_isStarNormal 📖	mathematical	—	IsStarProjection Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Set Complex Set.instHasSubset spectrum Complex.instCommSemiring Set.instInsert Complex.instZero Set.instSingletonSet Complex.instOne IsStarNormal	—	Complex.instNontrivial IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar IsScalarTower.right Algebra.to_smulCommClass isIdempotentElem_iff_spectrum_subset isStarProjection_iff_isIdempotentElem_and_isStarNormal

---

← Back to Index