StarOrder

📁 Source: Mathlib/Analysis/InnerProductSpace/StarOrder.lean

Statistics

Metric	Count
Definitions	0
Theorems spectrumRestricts, instNonnegSpectrumClassRealId, instStarOrderedRing, instStarOrderedRingRCLike	4
Total	4

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNonnegSpectrumClassRealId 📖	mathematical	—	NonnegSpectrumClass Real ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Real.instCommSemiring Real.partialOrder NonUnitalNormedRing.toNonUnitalRing NormedRing.toNonUnitalNormedRing toNormedRing DenselyNormedField.toNontriviallyNormedField instLoewnerPartialOrder Algebra.toModule semiring IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul QuasispectrumRestricts.nnreal_iff IsScalarTower.right Algebra.to_smulCommClass IsPositive.spectrumRestricts sub_zero
instStarOrderedRing 📖	mathematical	—	StarOrderedRing ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Complex.instNormedField InnerProductSpace.toNormedSpace Complex.instRCLike Semiring.toNonUnitalSemiring semiring IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup instLoewnerPartialOrder instStarRingId	—	instStarOrderedRingRCLike IsScalarTower.to_smulCommClass' IsScalarTower.complexToReal IsScalarTower.left UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self isScalarTower IsSelfAdjoint.instContinuousFunctionalCalculus IsStarNormal.instContinuousFunctionalCalculus
instStarOrderedRingRCLike 📖	mathematical	—	StarOrderedRing ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Semiring.toNonUnitalSemiring semiring IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup instLoewnerPartialOrder instStarRingId	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts IsScalarTower.right Algebra.to_smulCommClass ContinuousFunctionalCalculus.toNonUnital Real.instCompleteSpace IsPositive.isSelfAdjoint le_def IsPositive.spectrumRestricts AddSubmonoid.subset_closure IsSelfAdjoint.star_eq sq add_comm RingHomIsometric.ids eq_sub_iff_add_eq add_sub_cancel_left AddSubmonoid.closure_induction IsPositive.adjoint_conj isPositive_one isPositive_zero IsPositive.add

ContinuousLinearMap.IsPositive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
spectrumRestricts 📖	mathematical	ContinuousLinearMap.IsPositive	SpectrumRestricts NNReal Real ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace NNReal.instSemifield Real.instField ContinuousLinearMap.ring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup NNReal.instAlgebraOfReal Ring.toSemiring Algebra.id Real.instCommSemiring DFunLike.coe ContinuousMap Real.pseudoMetricSpace NNReal.instTopologicalSpace ContinuousMap.instFunLike ContinuousMap.realToNNReal	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SpectrumRestricts.nnreal_iff Mathlib.Tactic.Contrapose.contrapose₁ spectrum.notMem_iff IsUnit.sub_iff RingHomIsometric.ids sub_eq_add_neg map_neg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass ContinuousLinearMap.isUnit_of_forall_le_norm_inner_map LT.lt.le neg_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Algebra.algebraMap_eq_smul_one algebraMap_smul ContinuousLinearMap.coe_smul' Pi.smul_apply ContinuousLinearMap.one_apply inner_smul_left RCLike.algebraMap_eq_ofReal RCLike.conj_ofReal RCLike.re_ofReal_mul inner_self_eq_norm_sq mul_comm inner_add_left map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass covariant_swap_add_of_covariant_add IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le re_inner_nonneg_left RCLike.re_le_norm

---

← Back to Index