Star

📁 Source: Mathlib/Data/NNReal/Star.lean

Statistics

Metric	Count
Definitions instStarRingNNReal	1
Theorems instStarModuleNNRealOfReal, instStarModuleNNRealReal, instTrivialStarNNReal	3
Total	4

(root)

Definitions

Name	Category	Theorems
instStarRingNNReal 📖	CompOp	76 math math: range_cfcₙ_nnreal, CFC.monotoneOn_one_sub_one_add_inv, nnnorm_cfcₙ_nnreal_le_iff, Commute.cfcₙ_nnreal, NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply_comp_toReal, instStarModuleNNRealOfReal, cfcₙHom_nnreal_eq_restrict, instStarModuleNNRealReal, Continuous.cfc_nnreal', CFC.rpow_def, ContinuousOn.cfc_nnreal', IsGreatest.nnnorm_cfc_nnreal, NNReal.instContinuousMap.UniqueHom, nnnorm_cfcₙ_nnreal_lt, cfc_real_eq_nnreal, StarAlgHom.realContinuousMapOfNNReal_apply, IsGreatest.nnnorm_cfcₙ_nnreal, continuousOn_cfc_nnreal, cfc_nnreal_eq_real, CFC.nnrpow_def, NNReal.instStarOrderedRing, StarAlgHom.realContinuousMapOfNNReal_apply_comp_toReal, Nonneg.instNonUnitalIsometricContinuousFunctionalCalculus, Continuous.cfc_nnreal_of_mem_nhdsSet, Continuous.cfcₙ_nnreal, ContinuousAt.cfcₙ_nnreal, ContinuousOn.cfc_nnreal_of_mem_nhdsSet, cfcₙ_tsub, CFC.rpow_neg_one_eq_cfc_inv, ContinuousWithinAt.cfcₙ_nnreal, range_cfcₙ_nnreal_eq_image_cfcₙ_real, Filter.Tendsto.cfcₙ_nnreal, ContinuousOn.cfc_nnreal, nnnorm_cfcₙ_nnreal_lt_iff, nnnorm_cfc_nnreal_lt, NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply, cfcₙ_real_eq_nnreal, nnnorm_cfc_nnreal_le, ContinuousOn.cfcₙ_nnreal_of_mem_nhdsSet, cfc_nnreal_le_iff, Continuous.cfc_nnreal, nnnorm_cfc_nnreal_le_iff, Nonneg.instContinuousFunctionalCalculus, ContinuousMapZero.toContinuousMapHom_toNNReal, cfcHom_nnreal_eq_restrict, ContinuousOn.cfcₙ_nnreal', range_cfc_nnreal, Unitization.nnreal_cfcₙ_eq_cfc_inr, Continuous.cfcₙ_nnreal_of_mem_nhdsSet, apply_le_nnnorm_cfc_nnreal, range_cfc_nnreal_eq_image_cfc_real, NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_injective, StarAlgHom.realContinuousMapOfNNReal_injective, Nonneg.instNonUnitalContinuousFunctionalCalculus, CFC.sqrt_eq_cfc, instTrivialStarNNReal, Filter.Tendsto.cfc_nnreal, norm_cfcₙ_one_sub_one_add_inv_lt_one, continuousOn_cfcₙ_nnreal, cfcₙ_nnreal_eq_real, cfc_tsub, nnnorm_cfc_nnreal_lt_iff, Commute.cfc_nnreal, MonotoneOn.nnnorm_cfc, ContinuousOn.cfcₙ_nnreal, NNReal.instContinuousMapZero.UniqueHom, continuousOn_cfc_nnreal_setProd, ContinuousAt.cfc_nnreal, ContinuousWithinAt.cfc_nnreal, nnnorm_cfcₙ_nnreal_le, apply_le_nnnorm_cfcₙ_nnreal, continuousOn_cfcₙ_nnreal_setProd, MonotoneOn.nnnorm_cfcₙ, Continuous.cfcₙ_nnreal', Nonneg.instIsometricContinuousFunctionalCalculus, NNReal.instContinuousStar

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instStarModuleNNRealOfReal 📖	mathematical	—	StarModule NNReal InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal StarRing.toStarAddMonoid instStarRingNNReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero NNReal.instDistribMulActionOfReal Module.toDistribMulAction Real Real.semiring	—	StarModule.star_smul
instStarModuleNNRealReal 📖	mathematical	—	StarModule NNReal Real InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal StarRing.toStarAddMonoid instStarRingNNReal NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing instStarRingReal Algebra.toSMul instCommSemiringNNReal Real.semiring NNReal.instAlgebraOfReal Algebra.id Real.instCommSemiring	—	TrivialStar.star_trivial instTrivialStarReal instTrivialStarNNReal
instTrivialStarNNReal 📖	mathematical	—	TrivialStar NNReal InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal StarRing.toStarAddMonoid instStarRingNNReal	—	—

---

← Back to Index