RealImaginaryPart

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

Statistics

Metric	Count
Definitions	0
Theorems cfc_comp_im, cfc_comp_re, cfc_im_id, cfc_imaginaryPart, cfc_re_id, cfc_realPart, cfcₙ_comp_im, cfcₙ_comp_re, cfcₙ_im_id, cfcₙ_imaginaryPart, cfcₙ_re_id, cfcₙ_realPart, quasispectrum_imaginaryPart, quasispectrum_imaginaryPart', quasispectrum_realPart, quasispectrum_realPart', spectrum_imaginaryPart, spectrum_imaginaryPart', spectrum_realPart, spectrum_realPart'	20
Total	20

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cfc_comp_im 📖	mathematical	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace spectrum Real.instCommSemiring Algebra.complexToReal Ring.toSemiring AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal Algebra.toModule Complex Complex.instCommSemiring selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike imaginaryPart	cfc Complex IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Complex.instCommSemiring Complex.instStarRing NormedField.toMetricSpace Complex.instNormedField IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar Complex.ofReal Complex.im Real IsSelfAdjoint Real.instCommSemiring instStarRingReal Real.metricSpace NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal Algebra.complexToReal Ring.toSemiring IsSelfAdjoint.instContinuousFunctionalCalculus AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal Algebra.toModule selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule CommRing.toNonUnitalCommRing Real.commRing instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike imaginaryPart	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar instTrivialStarReal StarModule.complexToReal Continuous.comp_continuousOn Complex.continuous_ofReal ContinuousOn.comp spectrum_imaginaryPart' Continuous.continuousOn Complex.continuous_re Set.mapsTo_image instIsTopologicalRingReal instContinuousStarReal IsSelfAdjoint.instContinuousFunctionalCalculus cfc_real_eq_complex cfc_im_id cfc_comp' Continuous.comp_continuousOn' Complex.continuous_im
cfc_comp_re 📖	mathematical	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace spectrum Real.instCommSemiring Algebra.complexToReal Ring.toSemiring AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal Algebra.toModule Complex Complex.instCommSemiring selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike realPart	cfc Complex IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Complex.instCommSemiring Complex.instStarRing NormedField.toMetricSpace Complex.instNormedField IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar Complex.ofReal Complex.re Real IsSelfAdjoint Real.instCommSemiring instStarRingReal Real.metricSpace NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal Algebra.complexToReal Ring.toSemiring IsSelfAdjoint.instContinuousFunctionalCalculus AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal Algebra.toModule selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule CommRing.toNonUnitalCommRing Real.commRing instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike realPart	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar instTrivialStarReal StarModule.complexToReal Continuous.comp_continuousOn Complex.continuous_ofReal ContinuousOn.comp spectrum_realPart' Continuous.continuousOn Complex.continuous_re Set.mapsTo_image instIsTopologicalRingReal instContinuousStarReal IsSelfAdjoint.instContinuousFunctionalCalculus cfc_real_eq_complex cfc_re_id cfc_comp' Continuous.comp_continuousOn'
cfc_im_id 📖	mathematical	—	cfc Complex IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Complex.instCommSemiring Complex.instStarRing NormedField.toMetricSpace Complex.instNormedField IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar Complex.ofReal Complex.im AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal Algebra.toModule Ring.toSemiring selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule CommRing.toNonUnitalCommRing Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike imaginaryPart	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar instTrivialStarReal StarModule.complexToReal cfc.congr_simp mul_comm Complex.re_add_im cfc_id' realPart_add_I_smul_imaginaryPart AddLeftCancelSemigroup.toIsLeftCancelAdd instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero cfc_re_id cfc_const_mul Continuous.comp_continuousOn' Complex.continuous_ofReal Continuous.continuousOn Complex.continuous_im cfc_add Complex.continuous_re ContinuousOn.const_mul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing
cfc_imaginaryPart 📖	mathematical	ContinuousOn Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex spectrum Complex.instCommSemiring AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal Algebra.toModule Ring.toSemiring selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike imaginaryPart	cfc Complex IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Complex.instCommSemiring Complex.instStarRing NormedField.toMetricSpace Complex.instNormedField IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal Algebra.toModule Ring.toSemiring selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule CommRing.toNonUnitalCommRing Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike imaginaryPart Complex.ofReal Complex.im	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar instTrivialStarReal StarModule.complexToReal cfc_im_id cfc_comp' spectrum_imaginaryPart Continuous.comp_continuousOn' Complex.continuous_ofReal Continuous.continuousOn Complex.continuous_im
cfc_re_id 📖	mathematical	—	cfc Complex IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Complex.instCommSemiring Complex.instStarRing NormedField.toMetricSpace Complex.instNormedField IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar Complex.ofReal Complex.re AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal Algebra.toModule Ring.toSemiring selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule CommRing.toNonUnitalCommRing Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike realPart	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar instTrivialStarReal StarModule.complexToReal Nat.instAtLeastTwoHAddOfNat realPart_apply_coe cfc_id' cfc_star cfc_add continuousOn_id' ContinuousOn.star cfc_smul UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsScalarTower.complexToReal IsScalarTower.left Pi.isScalarTower IsScalarTower.right ContinuousOn.fun_add IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing cfc_congr Complex.re_eq_add_conj smul_one_smul div_eq_inv_mul Complex.ofReal_inv mul_one
cfc_realPart 📖	mathematical	ContinuousOn Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex spectrum Complex.instCommSemiring AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal Algebra.toModule Ring.toSemiring selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike realPart	cfc Complex IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Complex.instCommSemiring Complex.instStarRing NormedField.toMetricSpace Complex.instNormedField IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal Algebra.toModule Ring.toSemiring selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule CommRing.toNonUnitalCommRing Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike realPart Complex.ofReal Complex.re	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar instTrivialStarReal StarModule.complexToReal cfc_re_id cfc_comp' spectrum_realPart Continuous.comp_continuousOn' Complex.continuous_ofReal Continuous.continuousOn Complex.continuous_re
cfcₙ_comp_im 📖	mathematical	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace quasispectrum Real.instCommSemiring Module.complexToReal NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike imaginaryPart Real.instZero	cfcₙ Complex IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Complex.instCommSemiring Complex.instNontrivial Complex.instStarRing NormedField.toMetricSpace Complex.instNormedField IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar Complex.ofReal Complex.im Real IsSelfAdjoint Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal Module.complexToReal NonUnitalNonAssocRing.toAddCommGroup IsScalarTower.complexToReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul SMulCommClass.complexToReal IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus AddSubgroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule CommRing.toNonUnitalCommRing Real.commRing instTrivialStarReal StarModule.complexToReal LinearMap.instFunLike imaginaryPart	—	Complex.instNontrivial IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar instTrivialStarReal StarModule.complexToReal Continuous.comp_continuousOn Complex.continuous_ofReal ContinuousOn.comp quasispectrum_imaginaryPart' Continuous.continuousOn Complex.continuous_re Set.mapsTo_image Real.instNontrivial instIsTopologicalRingReal instContinuousStarReal IsScalarTower.complexToReal SMulCommClass.complexToReal IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus cfcₙ_real_eq_complex cfcₙ_im_id cfcₙ_comp' Continuous.comp_continuousOn' Complex.continuous_im
cfcₙ_comp_re 📖	mathematical	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace quasispectrum Real.instCommSemiring Module.complexToReal NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike realPart Real.instZero	cfcₙ Complex IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Complex.instCommSemiring Complex.instNontrivial Complex.instStarRing NormedField.toMetricSpace Complex.instNormedField IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar Complex.ofReal Complex.re Real IsSelfAdjoint Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal Module.complexToReal NonUnitalNonAssocRing.toAddCommGroup IsScalarTower.complexToReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul SMulCommClass.complexToReal IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus AddSubgroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule CommRing.toNonUnitalCommRing Real.commRing instTrivialStarReal StarModule.complexToReal LinearMap.instFunLike realPart	—	Complex.instNontrivial IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar instTrivialStarReal StarModule.complexToReal Continuous.comp_continuousOn Complex.continuous_ofReal ContinuousOn.comp quasispectrum_realPart' Continuous.continuousOn Complex.continuous_re Set.mapsTo_image Real.instNontrivial instIsTopologicalRingReal instContinuousStarReal IsScalarTower.complexToReal SMulCommClass.complexToReal IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus cfcₙ_real_eq_complex cfcₙ_re_id cfcₙ_comp' Continuous.comp_continuousOn'
cfcₙ_im_id 📖	mathematical	—	cfcₙ Complex IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Complex.instCommSemiring Complex.instNontrivial Complex.instStarRing NormedField.toMetricSpace Complex.instNormedField IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar Complex.ofReal Complex.im AddSubgroup AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule CommRing.toNonUnitalCommRing Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike imaginaryPart	—	Complex.instNontrivial IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar instTrivialStarReal StarModule.complexToReal cfcₙ.congr_simp mul_comm Complex.re_add_im cfcₙ_id' realPart_add_I_smul_imaginaryPart AddLeftCancelSemigroup.toIsLeftCancelAdd instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero cfcₙ_re_id cfcₙ_const_mul Continuous.comp_continuousOn' Complex.continuous_ofReal Continuous.continuousOn Complex.continuous_im cfcₙ_add Complex.continuous_re ContinuousOn.const_mul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing MulZeroClass.mul_zero
cfcₙ_imaginaryPart 📖	mathematical	ContinuousOn Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex quasispectrum Complex.instCommSemiring AddSubgroup AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike imaginaryPart Complex.instZero	cfcₙ Complex IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Complex.instCommSemiring Complex.instNontrivial Complex.instStarRing NormedField.toMetricSpace Complex.instNormedField IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar AddSubgroup AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule CommRing.toNonUnitalCommRing Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike imaginaryPart Complex.ofReal Complex.im	—	Complex.instNontrivial IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar instTrivialStarReal StarModule.complexToReal cfcₙ_im_id cfcₙ_comp' quasispectrum_imaginaryPart Continuous.comp_continuousOn' Complex.continuous_ofReal Continuous.continuousOn Complex.continuous_im
cfcₙ_re_id 📖	mathematical	—	cfcₙ Complex IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Complex.instCommSemiring Complex.instNontrivial Complex.instStarRing NormedField.toMetricSpace Complex.instNormedField IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar Complex.ofReal Complex.re AddSubgroup AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule CommRing.toNonUnitalCommRing Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike realPart	—	Complex.instNontrivial IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar instTrivialStarReal StarModule.complexToReal Nat.instAtLeastTwoHAddOfNat realPart_apply_coe cfcₙ_id' cfcₙ_star cfcₙ_add continuousOn_id' ContinuousOn.star star_zero cfcₙ_smul UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsScalarTower.complexToReal IsScalarTower.left Pi.isScalarTower IsScalarTower.right ContinuousOn.fun_add IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing add_zero cfcₙ_congr Complex.re_eq_add_conj smul_one_smul div_eq_inv_mul Complex.ofReal_inv mul_one
cfcₙ_realPart 📖	mathematical	ContinuousOn Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex quasispectrum Complex.instCommSemiring AddSubgroup AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike realPart Complex.instZero	cfcₙ Complex IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Complex.instCommSemiring Complex.instNontrivial Complex.instStarRing NormedField.toMetricSpace Complex.instNormedField IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar AddSubgroup AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule CommRing.toNonUnitalCommRing Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike realPart Complex.ofReal Complex.re	—	Complex.instNontrivial IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar instTrivialStarReal StarModule.complexToReal cfcₙ_re_id cfcₙ_comp' quasispectrum_realPart Continuous.comp_continuousOn' Complex.continuous_ofReal Continuous.continuousOn Complex.continuous_re
quasispectrum_imaginaryPart 📖	mathematical	—	quasispectrum Complex Complex.instCommSemiring AddSubgroup AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike imaginaryPart Set.image Complex.ofReal Complex.im	—	Complex.instNontrivial IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar instTrivialStarReal StarModule.complexToReal cfcₙ_im_id cfcₙ_map_quasispectrum Continuous.comp_continuousOn' Complex.continuous_ofReal Continuous.continuousOn Complex.continuous_im
quasispectrum_imaginaryPart' 📖	mathematical	—	quasispectrum Real Real.instCommSemiring Module.complexToReal NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike imaginaryPart Set.image Complex Complex.im Complex.instCommSemiring	—	Complex.instNontrivial IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar instTrivialStarReal StarModule.complexToReal QuasispectrumRestricts.image IsScalarTower.complexToReal IsScalarTower.left IsSelfAdjoint.quasispectrumRestricts Set.image_congr quasispectrum_imaginaryPart Set.image_image
quasispectrum_realPart 📖	mathematical	—	quasispectrum Complex Complex.instCommSemiring AddSubgroup AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike realPart Set.image Complex.ofReal Complex.re	—	Complex.instNontrivial IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar instTrivialStarReal StarModule.complexToReal cfcₙ_re_id cfcₙ_map_quasispectrum Continuous.comp_continuousOn' Complex.continuous_ofReal Continuous.continuousOn Complex.continuous_re
quasispectrum_realPart' 📖	mathematical	—	quasispectrum Real Real.instCommSemiring Module.complexToReal NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike realPart Set.image Complex Complex.re Complex.instCommSemiring	—	Complex.instNontrivial IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar instTrivialStarReal StarModule.complexToReal QuasispectrumRestricts.image IsScalarTower.complexToReal IsScalarTower.left IsSelfAdjoint.quasispectrumRestricts Set.image_congr quasispectrum_realPart Set.image_image
spectrum_imaginaryPart 📖	mathematical	—	spectrum Complex Complex.instCommSemiring AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal Algebra.toModule Ring.toSemiring selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike imaginaryPart Set.image Complex.ofReal Complex.im	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar instTrivialStarReal StarModule.complexToReal cfc_im_id cfc_map_spectrum Continuous.comp_continuousOn' Complex.continuous_ofReal Continuous.continuousOn Complex.continuous_im
spectrum_imaginaryPart' 📖	mathematical	—	spectrum Real Real.instCommSemiring Algebra.complexToReal Ring.toSemiring AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal Algebra.toModule Complex Complex.instCommSemiring selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike imaginaryPart Set.image Complex.im	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar instTrivialStarReal StarModule.complexToReal SpectrumRestricts.image IsScalarTower.complexToReal IsScalarTower.left IsSelfAdjoint.spectrumRestricts Set.image_congr spectrum_imaginaryPart Set.image_image
spectrum_realPart 📖	mathematical	—	spectrum Complex Complex.instCommSemiring AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal Algebra.toModule Ring.toSemiring selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike realPart Set.image Complex.ofReal Complex.re	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar instTrivialStarReal StarModule.complexToReal cfc_re_id cfc_map_spectrum Continuous.comp_continuousOn' Complex.continuous_ofReal Continuous.continuousOn Complex.continuous_re
spectrum_realPart' 📖	mathematical	—	spectrum Real Real.instCommSemiring Algebra.complexToReal Ring.toSemiring AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Module.complexToReal Algebra.toModule Complex Complex.instCommSemiring selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LinearMap.instFunLike realPart Set.image Complex.re	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar instTrivialStarReal StarModule.complexToReal SpectrumRestricts.image IsScalarTower.complexToReal IsScalarTower.left IsSelfAdjoint.spectrumRestricts Set.image_congr spectrum_realPart Set.image_image

---

← Back to Index