Unitary

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

Statistics

Metric	Count
Definitions	0
Theorems cfc_unitary_iff, mem_unitary_of_spectrum_subset_unitary, spectrum_subset_unitary_of_mem_unitary, unitary_iff_isStarNormal_and_spectrum_subset_unitary	4
Total	4

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cfc_unitary_iff 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum CommRing.toCommSemiring	Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring cfc IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	IsTopologicalRing.toIsTopologicalSemiring Commute.eq IsStarNormal.star_comm_self IsStarNormal.cfc_map cfc_one cfc_star cfc_mul ContinuousOn.star cfc_eq_cfc_iff_eqOn ContinuousOn.fun_mul IsTopologicalSemiring.toContinuousMul Continuous.continuousOn continuous_one
mem_unitary_of_spectrum_subset_unitary 📖	mathematical	Set Complex Set.instHasSubset spectrum Complex.instCommSemiring SetLike.coe Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Complex.instStarRing	Ring.toSemiring SetLike.instMembership	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar unitary_iff_isStarNormal_and_spectrum_subset_unitary
spectrum_subset_unitary_of_mem_unitary 📖	mathematical	Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring	Set Complex Set.instHasSubset spectrum Complex.instCommSemiring SetLike.coe Complex.instSemiring Complex.instStarRing	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar unitary_iff_isStarNormal_and_spectrum_subset_unitary
unitary_iff_isStarNormal_and_spectrum_subset_unitary 📖	mathematical	—	Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsStarNormal 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 SetLike.coe Complex.instSemiring Complex.instStarRing	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar isStarNormal_of_mem_unitary cfc_id cfc_unitary_iff continuousOn_id' Set.subset_def

---

← Back to Index