Documentation Verification Report

Spectrum

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

Statistics

Metric	Count
Definitions	0
Theorems `instStarHomClass`, `le_nnnorm_of_mem_quasispectrum`, `im_eq_zero_of_mem_spectrum`, `isConnected_spectrum_compl`, `mem_spectrum_eq_re`, `spectralRadius_eq_nnnorm`, `toReal_spectralRadius_complex_eq_norm`, `val_re_map_spectrum`, `spectralRadius_eq_nnnorm`, `instContinuousLinearMapClassComplex`, `nnnorm_apply_le`, `norm_apply_le`, `isometry`, `nnnorm_map`, `norm_map`, `coe_isUnit`, `mem_spectrum_iff`, `spectrum_eq`, `spectrum_subset_circle`, `instStarHomClass`, `instStarHomClass`, `mem_spectrum_eq_re`, `val_re_map_spectrum`, `norm_eq_one_of_unitary`, `subset_circle_of_unitary`, `spectrum_subset_circle`	26
Total	26

AlgHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instStarHomClass` 📖	mathematical	—	`StarHomClass` `Complex` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `CStarAlgebra.toNormedRing` `StarRing.toStarAddMonoid` `CStarAlgebra.toStarRing` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing` `CommCStarAlgebra.toNonUnitalCommCStarAlgebra` `instCommCStarAlgebraComplex` `Complex.instStarRing`	—	`WeakDual.Complex.instStarHomClass`

CStarAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_nnnorm_of_mem_quasispectrum` 📖	mathematical	`NNReal` `Set` `Set.instMembership` `quasispectrum` `instCommSemiringNNReal` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `NNReal.instModuleOfReal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NormedSpace.toModule` `Real` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedSpace.complexToReal` `NonUnitalCStarAlgebra.toNormedSpace`	`Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`NonUnitalCStarAlgebra.toIsScalarTower` `NonUnitalCStarAlgebra.toSMulCommClass` `CStarRing.instRegularNormedAlgebra` `NonUnitalCStarAlgebra.toCStarRing` `Unitization.nnnorm_inr` `spectrum.le_nnnorm_of_mem` `Unitization.instCompleteSpace` `Complex.instCompleteSpace` `NonUnitalCStarAlgebra.toCompleteSpace` `Unitization.instNormOneClass` `NNReal.instIsScalarTowerOfReal` `IsScalarTower.complexToReal` `IsScalarTower.left` `Unitization.quasispectrum_eq_spectrum_inr'`

IsSelfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`im_eq_zero_of_mem_spectrum` 📖	mathematical	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `CStarAlgebra.toNormedRing` `StarRing.toStarAddMonoid` `CStarAlgebra.toStarRing` `Complex` `Set` `Set.instMembership` `spectrum` `Complex.instCommSemiring` `NormedAlgebra.toAlgebra` `Complex.instNormedField` `NormedRing.toSeminormedRing` `CStarAlgebra.toNormedAlgebra`	`Complex.im` `Real` `Real.instZero`	—	`mem_spectrum_eq_re` `Complex.ofReal_im`
`isConnected_spectrum_compl` 📖	mathematical	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `CStarAlgebra.toNormedRing` `StarRing.toStarAddMonoid` `CStarAlgebra.toStarRing`	`IsConnected` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `Compl.compl` `Set` `Set.instCompl` `spectrum` `Complex.instCommSemiring` `NormedAlgebra.toAlgebra` `Complex.instNormedField` `NormedRing.toSeminormedRing` `CStarAlgebra.toNormedAlgebra`	—	`IsConnected.union` `Filter.NeBot.nonempty_of_mem` `NontriviallyNormedField.cobounded_neBot` `Filter.mem_map` `AntilipschitzWith.tendsto_cobounded` `Isometry.antilipschitz` `Complex.isometry_ofReal` `Bornology.IsBounded.compl` `spectrum.isBounded` `CStarAlgebra.toCompleteSpace` `Set.Nonempty.mono` `Set.instReflSubset` `Set.Nonempty.image` `Complex.isConnected_of_upperHalfPlane` `Set.subset_inter` `im_eq_zero_of_mem_spectrum` `Set.mem_setOf_eq` `le_of_lt` `Set.inter_subset_right` `Complex.isConnected_of_lowerHalfPlane` `Set.inter_univ` `Set.eq_univ_of_forall` `le_total` `Set.setOf_or` `Set.inter_union_distrib_left`
`mem_spectrum_eq_re` 📖	mathematical	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `CStarAlgebra.toNormedRing` `StarRing.toStarAddMonoid` `CStarAlgebra.toStarRing` `Complex` `Set` `Set.instMembership` `spectrum` `Complex.instCommSemiring` `NormedAlgebra.toAlgebra` `Complex.instNormedField` `NormedRing.toSeminormedRing` `CStarAlgebra.toNormedAlgebra`	`Complex.ofReal` `Complex.re`	—	`Complex.instCharZero` `NonUnitalSeminormedRing.toIsTopologicalRing` `NormedSpace.exp_mem_unitary_of_mem_skewAdjoint` `CStarAlgebra.toCompleteSpace` `NormedStarGroup.to_continuousStar` `CStarRing.to_normedStarGroup` `CStarAlgebra.toCStarRing` `smul_mem_skewAdjoint` `Complex.conj_I` `Complex.I_ne_zero` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `spectrum.exp_mem_exp` `spectrum.smul_mem_smul_iff` `Complex.ext` `Complex.ofReal_re` `NormedSpace.exp.congr_simp` `Complex.I_mul` `Complex.norm_exp` `spectrum.subset_circle_of_unitary`
`spectralRadius_eq_nnnorm` 📖	mathematical	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `CStarAlgebra.toNormedRing` `StarRing.toStarAddMonoid` `CStarAlgebra.toStarRing`	`spectralRadius` `Complex` `Complex.instNormedField` `NormedAlgebra.toAlgebra` `NormedRing.toSeminormedRing` `CStarAlgebra.toNormedAlgebra` `ENNReal.ofNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `CStarAlgebra.toNonUnitalCStarAlgebra`	—	`tendsto_const_nhds` `tendsto_nhds_unique` `ENNReal.instT2Space` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Nat.instAtLeastTwoHAddOfNat` `nnnorm_pow_two_pow` `CStarAlgebra.toCStarRing` `ENNReal.coe_pow` `ENNReal.rpow_natCast` `ENNReal.rpow_mul` `Nat.cast_pow` `one_div` `mul_inv_cancel₀` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Real.instNontrivial` `RCLike.charZero_rclike` `ENNReal.rpow_one` `Filter.Tendsto.comp` `spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius` `CStarAlgebra.toCompleteSpace` `tendsto_pow_atTop_atTop_of_one_lt` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `one_lt_two` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`toReal_spectralRadius_complex_eq_norm` 📖	mathematical	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `CStarAlgebra.toNormedRing` `StarRing.toStarAddMonoid` `CStarAlgebra.toStarRing`	`ENNReal.toReal` `spectralRadius` `Complex` `Complex.instNormedField` `NormedAlgebra.toAlgebra` `NormedRing.toSeminormedRing` `CStarAlgebra.toNormedAlgebra` `Norm.norm` `NormedRing.toNorm`	—	`spectralRadius_eq_nnnorm`
`val_re_map_spectrum` 📖	mathematical	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `CStarAlgebra.toNormedRing` `StarRing.toStarAddMonoid` `CStarAlgebra.toStarRing`	`spectrum` `Complex` `Complex.instCommSemiring` `NormedAlgebra.toAlgebra` `Complex.instNormedField` `NormedRing.toSeminormedRing` `CStarAlgebra.toNormedAlgebra` `Set.image` `Real` `Complex.ofReal` `Complex.re`	—	`le_antisymm` `mem_spectrum_eq_re`

IsStarNormal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`spectralRadius_eq_nnnorm` 📖	mathematical	—	`spectralRadius` `Complex` `Complex.instNormedField` `NormedRing.toRing` `CStarAlgebra.toNormedRing` `NormedAlgebra.toAlgebra` `NormedRing.toSeminormedRing` `CStarAlgebra.toNormedAlgebra` `ENNReal.ofNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `CStarAlgebra.toNonUnitalCStarAlgebra`	—	`StrictMono.injective` `ENNReal.pow_right_strictMono` `two_ne_zero` `ENNReal.rpow_natCast` `ENNReal.rpow_mul` `mul_comm` `ENNReal.coe_pow` `sq` `CStarRing.nnnorm_star_mul_self` `CStarAlgebra.toCStarRing` `Commute.mul_pow` `star_comm_self'` `star_pow` `Filter.Tendsto.comp` `Continuous.tendsto` `ENNReal.continuous_pow` `spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius` `CStarAlgebra.toCompleteSpace` `IsSelfAdjoint.spectralRadius_eq_nnnorm` `IsSelfAdjoint.star_mul_self` `ENNReal.coe_mul` `tendsto_nhds_unique` `ENNReal.instT2Space` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat`

NonUnitalStarAlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instContinuousLinearMapClassComplex` 📖	mathematical	—	`ContinuousLinearMapClass` `Complex` `Complex.instSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalCStarAlgebra.toNormedSpace`	—	`NonUnitalAlgHomClass.instLinearMapClass` `AddMonoidHomClass.continuous_of_bound` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `one_mul` `nnnorm_apply_le`
`nnnorm_apply_le` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `DFunLike.coe`	—	`NonUnitalCStarAlgebra.toIsScalarTower` `NonUnitalCStarAlgebra.toSMulCommClass` `IsScalarTower.left` `iSup_le_iSup_of_subset` `AlgHom.spectrum_apply_subset` `StarAlgHom.instAlgHomClass` `ENNReal.coe_le_coe` `IsSelfAdjoint.spectralRadius_eq_nnnorm` `IsSelfAdjoint.map` `StarAlgHom.instStarHomClass` `nonneg_le_nonneg_of_sq_le_sq` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `IsOrderedRing.toMulPosMono` `NNReal.instIsOrderedRing` `zero_le'` `NonUnitalCStarAlgebra.toStarModule` `Unitization.instCStarRing` `NonUnitalCStarAlgebra.toCStarRing` `CStarAlgebra.toCStarRing` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `IsSelfAdjoint.star_mul_self` `CStarAlgebra.toStarModule` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `zero_add` `Unitization.nnnorm_inr`
`norm_apply_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `NonUnitalNormedRing.toNorm` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `DFunLike.coe`	—	`nnnorm_apply_le`

StarAlgEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isometry` 📖	mathematical	—	`Isometry` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NonUnitalNormedRing.toMetricSpace` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `DFunLike.coe` `EquivLike.toFunLike`	—	`AddMonoidHomClass.isometry_of_norm` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `instNonUnitalAlgHomClassOfNonUnitalAlgEquivClass` `norm_map`
`nnnorm_map` 📖	mathematical	—	`NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `DFunLike.coe` `EquivLike.toFunLike`	—	`le_antisymm` `NonUnitalStarAlgHom.nnnorm_apply_le` `instNonUnitalAlgHomClassOfNonUnitalAlgEquivClass` `symm_apply_apply` `instNonUnitalAlgEquivClass` `NonUnitalStarRingHomClass.toStarHomClass` `NonUnitalAlgHomClass.toNonUnitalRingHomClass` `NonUnitalStarAlgHomClass.instNonUnitalStarRingHomClassOfStarHomClass` `RingEquivClass.toNonUnitalRingHomClass` `NonUnitalAlgEquivClass.toRingEquivClass` `StarRingEquivClass.instNonUnitalStarRingHomClass` `instStarRingEquivClass`
`norm_map` 📖	mathematical	—	`Norm.norm` `NonUnitalNormedRing.toNorm` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `DFunLike.coe` `EquivLike.toFunLike`	—	`nnnorm_map`

StarSubalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_isUnit` 📖	mathematical	—	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `CStarAlgebra.toNormedRing` `StarSubalgebra` `Complex` `Complex.instCommSemiring` `Complex.instStarRing` `CStarAlgebra.toStarRing` `NormedAlgebra.toAlgebra` `Complex.instNormedField` `NormedRing.toSeminormedRing` `CStarAlgebra.toNormedAlgebra` `SetLike.instMembership` `setLike` `SubringClass.toNormedRing` `subringClass` `Complex.commRing`	—	`subringClass` `IsUnit.mul` `IsUnit.star` `starMemClass` `Subalgebra.spectrum_eq_of_isPreconnected_compl` `CStarAlgebra.toCompleteSpace` `smulMemClass` `IsConnected.isPreconnected` `subsemiringClass` `IsSelfAdjoint.isConnected_spectrum_compl` `IsSelfAdjoint.map` `StarAlgHom.instStarHomClass` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass` `spectrum.zero_notMem_iff` `IsSelfAdjoint.star_mul_self` `NonUnitalSubsemiringClass.mulMemClass` `SubringClass.toSubsemiringClass` `MulMemClass.coe_mul` `StarMemClass.coe_star` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `IsUnit.val_inv_mul` `mul_assoc` `IsSelfAdjoint.mul_star_self` `IsUnit.mul_val_inv` `left_inv_eq_right_inv` `IsUnit.map` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `StarAlgHom.instAlgHomClass`
`mem_spectrum_iff` 📖	mathematical	—	`Complex` `Set` `Set.instMembership` `spectrum` `StarSubalgebra` `Complex.instCommSemiring` `Complex.instStarRing` `Ring.toSemiring` `NormedRing.toRing` `CStarAlgebra.toNormedRing` `CStarAlgebra.toStarRing` `NormedAlgebra.toAlgebra` `Complex.instNormedField` `NormedRing.toSeminormedRing` `CStarAlgebra.toNormedAlgebra` `SetLike.instMembership` `setLike` `SubringClass.toNormedRing` `subringClass` `Complex.commRing` `algebra`	—	`subringClass` `not_iff_not` `coe_isUnit`
`spectrum_eq` 📖	mathematical	—	`spectrum` `Complex` `StarSubalgebra` `Complex.instCommSemiring` `Complex.instStarRing` `Ring.toSemiring` `NormedRing.toRing` `CStarAlgebra.toNormedRing` `CStarAlgebra.toStarRing` `NormedAlgebra.toAlgebra` `Complex.instNormedField` `NormedRing.toSeminormedRing` `CStarAlgebra.toNormedAlgebra` `SetLike.instMembership` `setLike` `SubringClass.toNormedRing` `subringClass` `Complex.commRing` `algebra`	—	`Set.ext` `subringClass` `mem_spectrum_iff`

Unitary

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`spectrum_subset_circle` 📖	mathematical	—	`Set` `Set.instHasSubset` `spectrum` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `NormedRing.toRing` `NormedAlgebra.toAlgebra` `NormedRing.toSeminormedRing` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Metric.sphere` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real` `Real.instOne`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `spectrum.of_subsingleton` `mem_sphere_zero_iff_norm` `le_antisymm` `CStarRing.norm_coe_unitary` `spectrum.norm_le_norm_of_mem` `CStarRing.instNormOneClassOfNontrivial` `spectrum.ne_zero_of_mem_of_unit` `val_toUnits_apply` `norm_inv` `Set.mem_inv` `spectrum.map_inv` `inv_inv` `CStarRing.norm_of_mem_unitary` `inv_one` `inv_le_of_inv_le₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `norm_pos_iff`

WeakDual.CharacterSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instStarHomClass` 📖	mathematical	—	`StarHomClass` `Set.Elem` `WeakDual` `Complex` `Complex.instCommSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `IsTopologicalSemiring.toContinuousAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing` `CommCStarAlgebra.toNonUnitalCommCStarAlgebra` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `Complex.instNormedField` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Algebra.toSMul` `Algebra.id` `Ring.uniformContinuousConstSMul` `Complex.instRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NormedRing.toRing` `CStarAlgebra.toNormedRing` `NormedSpace.toModule` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `CStarAlgebra.toNonUnitalCStarAlgebra` `NonUnitalCStarAlgebra.toNormedSpace` `NormedRing.toSeminormedRing` `WeakDual.characterSpace` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `CStarAlgebra.toStarRing` `Complex.instStarRing` `instFunLike`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `AlgHomClass.instStarHomClass` `instAlgHomClass` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass`

WeakDual.Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instStarHomClass` 📖	mathematical	—	`StarHomClass` `Complex` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `CStarAlgebra.toNormedRing` `StarRing.toStarAddMonoid` `CStarAlgebra.toStarRing` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing` `CommCStarAlgebra.toNonUnitalCommCStarAlgebra` `instCommCStarAlgebraComplex` `Complex.instStarRing`	—	`AlgHom.apply_mem_spectrum` `Complex.instNontrivial` `selfAdjoint.val_re_map_spectrum` `CStarAlgebra.toStarModule` `RCLike.star_def` `RCLike.conj_ofReal` `instTrivialStarReal` `StarModule.complexToReal` `realPart_add_I_smul_imaginaryPart` `StarAddMonoid.star_add` `selfAdjoint.star_val_eq` `StarModule.star_smul` `map_add` `SemilinearMapClass.toAddHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `AlgHom.instContinuousLinearMapClassOfAlgHomClass` `CStarAlgebra.toCompleteSpace` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass`

selfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_spectrum_eq_re` 📖	mathematical	`Complex` `Set` `Set.instMembership` `spectrum` `Complex.instCommSemiring` `NormedRing.toRing` `CStarAlgebra.toNormedRing` `NormedAlgebra.toAlgebra` `Complex.instNormedField` `NormedRing.toSeminormedRing` `CStarAlgebra.toNormedAlgebra` `AddSubgroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `CStarAlgebra.toNonUnitalCStarAlgebra` `SetLike.instMembership` `AddSubgroup.instSetLike` `selfAdjoint` `StarRing.toStarAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `CStarAlgebra.toStarRing`	`Complex.ofReal` `Complex.re`	—	`IsSelfAdjoint.mem_spectrum_eq_re` `Subtype.prop`
`val_re_map_spectrum` 📖	mathematical	—	`spectrum` `Complex` `Complex.instCommSemiring` `NormedRing.toRing` `CStarAlgebra.toNormedRing` `NormedAlgebra.toAlgebra` `Complex.instNormedField` `NormedRing.toSeminormedRing` `CStarAlgebra.toNormedAlgebra` `AddSubgroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `CStarAlgebra.toNonUnitalCStarAlgebra` `SetLike.instMembership` `AddSubgroup.instSetLike` `selfAdjoint` `StarRing.toStarAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `CStarAlgebra.toStarRing` `Set.image` `Real` `Complex.ofReal` `Complex.re`	—	`IsSelfAdjoint.val_re_map_spectrum`

spectrum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`norm_eq_one_of_unitary` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Set` `Set.instMembership` `spectrum` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `NormedAlgebra.toAlgebra` `NormedRing.toSeminormedRing`	`Norm.norm` `NormedField.toNorm` `Real` `Real.instOne`	—	`sub_zero` `subset_circle_of_unitary`
`subset_circle_of_unitary` 📖	mathematical	`Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring`	`Set` `Set.instHasSubset` `spectrum` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `NormedAlgebra.toAlgebra` `NormedRing.toSeminormedRing` `Metric.sphere` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real` `Real.instOne`	—	`Unitary.spectrum_subset_circle`

unitary

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`spectrum_subset_circle` 📖	mathematical	—	`Set` `Set.instHasSubset` `spectrum` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `NormedRing.toRing` `NormedAlgebra.toAlgebra` `NormedRing.toSeminormedRing` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Metric.sphere` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real` `Real.instOne`	—	`Unitary.spectrum_subset_circle`

---

← Back to Index