Pi

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

Statistics

Metric	Count
Definitions	0
Theorems cfc_map_pi, cfc_map_prod, cfcₙ_map_pi, cfcₙ_map_prod	4
Total	4

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cfc_map_pi 📖	mathematical	IsScalarTower Algebra.toSMul CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring ContinuousFunctionalCalculus ContinuousMap.UniqueHom ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Set.iUnion spectrum	cfc Pi.topologicalSpace Pi.ring Pi.instStarRingForall Semiring.toNonUnitalSemiring Pi.algebra	—	StarAlgHom.map_cfc Pi.spectrum_eq continuous_apply
cfc_map_prod 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Set Set.instUnion spectrum	cfc instTopologicalSpaceProd Prod.instRing Prod.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Prod.algebra Ring.toSemiring	—	StarAlgHom.map_cfc Prod.isScalarTower Prod.spectrum_eq continuous_fst continuous_snd
cfcₙ_map_pi 📖	mathematical	IsScalarTower Algebra.toSMul CommSemiring.toSemiring CommRing.toCommSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring SMulCommClass NonUnitalNonAssocSemiring.toDistribSMul NonUnitalContinuousFunctionalCalculus ContinuousMapZero.UniqueHom ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Set.iUnion quasispectrum	cfcₙ Pi.nonUnitalRing Pi.instStarRingForall NonUnitalRing.toNonUnitalSemiring Pi.topologicalSpace Pi.module Pi.isScalarTower' SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Pi.smulCommClass'	—	Pi.isScalarTower' Pi.smulCommClass' isEmpty_or_nonempty Unique.instSubsingleton NonUnitalStarAlgHom.map_cfcₙ Pi.isScalarTower Pi.quasispectrum_eq continuous_apply cfcₙ_apply_of_not_map_zero
cfcₙ_map_prod 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Set Set.instUnion quasispectrum	cfcₙ Prod.instNonUnitalRing Prod.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing instTopologicalSpaceProd Prod.instModule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Prod.isScalarTowerBoth Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Prod.smulCommClassBoth	—	Prod.isScalarTowerBoth Prod.smulCommClassBoth NonUnitalStarAlgHom.map_cfcₙ Prod.isScalarTower Prod.quasispectrum_eq continuous_fst continuous_snd cfcₙ_apply_of_not_map_zero Prod.mk_zero_zero

---

← Back to Index