Hom

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

Statistics

Metric	Count
Definitions	0
Theorems map_spectrum_real, isometry, nnnorm_map, norm_map	4
Total	4

IsSelfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_spectrum_real 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing CStarAlgebra.toNormedRing StarRing.toStarAddMonoid CStarAlgebra.toStarRing DFunLike.coe	spectrum Real Real.instCommSemiring NormedAlgebra.toAlgebra Real.normedField NormedRing.toSeminormedRing NormedAlgebra.complexToReal CStarAlgebra.toNormedAlgebra	—	IsScalarTower.complexToReal IsScalarTower.left AlgHom.spectrum_apply_subset StarAlgHom.instAlgHomClass Set.eq_of_subset_of_subset exists_continuous_zero_one_of_isClosed T4Space.toNormalSpace T5Space.toT4Space OrderTopology.t5Space instOrderTopologyReal spectrum.isClosed CStarAlgebra.toCompleteSpace isClosed_singleton T5Space.toT1Space IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal instContinuousFunctionalCalculus IsStarNormal.instContinuousFunctionalCalculus StarAlgHomClass.map_cfc Real.instContinuousMapUniqueHom TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Continuous.continuousOn ContinuousMapClass.map_continuous ContinuousMap.instContinuousMapClass ContinuousSemilinearMapClass.toContinuousMapClass NonUnitalStarAlgHom.instContinuousLinearMapClassComplex AlgHom.instNonUnitalAlgHomClassOfAlgHomClass map cfc_congr cfc_zero zero_ne_one NeZero.charZero_one RCLike.charZero_rclike cfc_eq_cfc_iff_eqOn continuous_zero map_eq_zero_iff MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass Set.mem_singleton

NonUnitalStarAlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isometry 📖	mathematical	DFunLike.coe	Isometry EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NonUnitalNormedRing.toMetricSpace NonUnitalCStarAlgebra.toNonUnitalNormedRing	—	AddMonoidHomClass.isometry_of_norm DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass norm_map
nnnorm_map 📖	mathematical	DFunLike.coe	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing	—	norm_map
norm_map 📖	mathematical	DFunLike.coe	Norm.norm NonUnitalNormedRing.toNorm NonUnitalCStarAlgebra.toNonUnitalNormedRing	—	NonUnitalCStarAlgebra.toIsScalarTower NonUnitalCStarAlgebra.toSMulCommClass IsScalarTower.left CStarRing.instRegularNormedAlgebra NonUnitalCStarAlgebra.toCStarRing sq_eq_sq₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg NonUnitalCStarAlgebra.toStarModule sq Unitization.instCStarRing CStarAlgebra.toCStarRing StarAlgHom.instStarHomClass NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass StarAlgHom.instAlgHomClass IsSelfAdjoint.star_mul_self IsScalarTower.complexToReal IsSelfAdjoint.toReal_spectralRadius_eq_norm IsSelfAdjoint.map iSup_congr_Prop IsSelfAdjoint.map_spectrum_real Unitization.starMap_inr Unitization.norm_inr Unitization.starMap_injective

---

← Back to Index