Documentation Verification Report

Isometric

📁 Source: Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Isometric.lean

Statistics

Metric	Count
Definitions	0
Theorems `norm_mul_mul_self_of_nonneg`, `norm_mul_mul_self_of_nonneg'`, `continuousOn_nnrpow`, `continuousOn_rpow`, `continuousOn_sqrt`, `nnnorm_nnrpow`, `nnnorm_rpow`, `nnnorm_sqrt`, `norm_mul_mul_star_self_of_nonneg`, `norm_nnrpow`, `norm_rpow`, `norm_sqrt`, `norm_star_mul_mul_self_of_nonneg`	13
Total	13

CFC

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousOn_nnrpow` 📖	mathematical	—	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NNReal` `instPowNNReal` `NonUnitalNormedRing.toNonUnitalRing` `NormedSpace.toModule` `Real` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus` `IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `StarRing.toStarAddMonoid` `Real.instCommSemiring` `Real.instNontrivial` `instStarRingReal` `Real.metricSpace` `IsTopologicalRing.toIsTopologicalSemiring` `MetricSpace.toPseudoMetricSpace` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `instIsTopologicalRingReal` `instContinuousStarReal` `NonUnitalNormedRing.toMetricSpace` `setOf` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Real.instNontrivial` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus` `eq_zero_or_pos` `nnrpow_zero` `continuousOn_const` `ContinuousOn.cfcₙ_nnreal_of_mem_nhdsSet` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `IsTopologicalRing.toIsSemitopologicalRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `Filter.univ_mem` `continuousOn_id` `NNReal.continuousOn_rpow_const` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero`
`continuousOn_rpow` 📖	mathematical	—	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `Real` `instPowReal` `NormedRing.toRing` `NormedAlgebra.toAlgebra` `Real.normedField` `IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus` `IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarRing.toStarAddMonoid` `Real.instCommSemiring` `instStarRingReal` `Real.metricSpace` `IsTopologicalRing.toIsTopologicalSemiring` `MetricSpace.toPseudoMetricSpace` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `instIsTopologicalRingReal` `instContinuousStarReal` `NormedRing.toMetricSpace` `setOf` `IsStrictlyPositive` `Preorder.toLE` `PartialOrder.toPreorder` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `ContinuousOn.cfc_nnreal_of_mem_nhdsSet` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `IsTopologicalRing.toIsSemitopologicalRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `nhdsSet_iUnion` `IsOpen.mem_nhdsSet` `isOpen_compl_singleton` `T5Space.toT1Space` `OrderTopology.t5Space` `NNReal.instOrderTopology` `spectrum.zero_notMem` `IsStrictlyPositive.isUnit` `continuousOn_id` `IsStrictlyPositive.nonneg` `NNReal.continuousOn_rpow_const`
`continuousOn_sqrt` 📖	mathematical	—	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `sqrt` `NonUnitalNormedRing.toNonUnitalRing` `NormedSpace.toModule` `Real` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus` `IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `StarRing.toStarAddMonoid` `Real.instCommSemiring` `Real.instNontrivial` `instStarRingReal` `Real.metricSpace` `IsTopologicalRing.toIsTopologicalSemiring` `MetricSpace.toPseudoMetricSpace` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `instIsTopologicalRingReal` `instContinuousStarReal` `NonUnitalNormedRing.toMetricSpace` `setOf` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Real.instNontrivial` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `ContinuousOn.cfcₙ_nnreal_of_mem_nhdsSet` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `IsTopologicalRing.toIsSemitopologicalRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `Filter.univ_mem` `continuousOn_id` `Continuous.continuousOn` `NNReal.continuous_sqrt` `NNReal.sqrt_zero`
`nnnorm_nnrpow` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `NNReal.instPartialOrder` `NNReal.instZero` `Preorder.toLE` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing`	`NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NNReal` `instPowNNReal` `NonUnitalNormedRing.toNonUnitalRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NormedSpace.toModule` `Real` `Real.normedField` `NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus` `IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `StarRing.toStarAddMonoid` `Real.instCommSemiring` `Real.instNontrivial` `instStarRingReal` `Real.metricSpace` `IsTopologicalRing.toIsTopologicalSemiring` `MetricSpace.toPseudoMetricSpace` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `instIsTopologicalRingReal` `instContinuousStarReal` `NonUnitalNormedRing.toMetricSpace` `NNReal.instPowReal` `NNReal.toReal`	—	`Real.instNontrivial` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `MonotoneOn.nnnorm_cfcₙ` `Monotone.monotoneOn` `NNReal.monotone_nnrpow_const` `NNReal.continuousOn_rpow_const` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero`
`nnnorm_rpow` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	`NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `Real` `instPowReal` `NormedRing.toRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedAlgebra.toAlgebra` `Real.normedField` `IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus` `IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarRing.toStarAddMonoid` `Real.instCommSemiring` `instStarRingReal` `Real.metricSpace` `IsTopologicalRing.toIsTopologicalSemiring` `MetricSpace.toPseudoMetricSpace` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `instIsTopologicalRingReal` `instContinuousStarReal` `NormedRing.toMetricSpace` `NNReal` `NNReal.instPowReal`	—	`IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus` `CanLift.prf` `NNReal.canLift` `LT.lt.le` `Algebra.to_smulCommClass` `IsScalarTower.right` `ContinuousFunctionalCalculus.toNonUnital` `nnrpow_eq_rpow` `IsTopologicalRing.toIsSemitopologicalRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus` `Real.instNontrivial` `IsometricContinuousFunctionalCalculus.toNonUnital` `nnnorm_nnrpow`
`nnnorm_sqrt` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing`	`NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `sqrt` `NonUnitalNormedRing.toNonUnitalRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NormedSpace.toModule` `Real` `Real.normedField` `NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus` `IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `StarRing.toStarAddMonoid` `Real.instCommSemiring` `Real.instNontrivial` `instStarRingReal` `Real.metricSpace` `IsTopologicalRing.toIsTopologicalSemiring` `MetricSpace.toPseudoMetricSpace` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `instIsTopologicalRingReal` `instContinuousStarReal` `NonUnitalNormedRing.toMetricSpace` `DFunLike.coe` `OrderIso` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `NNReal.instPartialOrder` `instFunLikeOrderIso` `NNReal.sqrt`	—	`Real.instNontrivial` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus` `Nat.instAtLeastTwoHAddOfNat` `sqrt_eq_nnrpow` `NNReal.sqrt_eq_rpow` `nnnorm_nnrpow` `one_div` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono`
`norm_mul_mul_star_self_of_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing`	`Norm.norm` `NonUnitalNormedRing.toNorm` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `Real` `Monoid.toPow` `Real.instMonoid` `sqrt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup`	—	`Real.instNontrivial` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `LE.le.star_eq` `sqrt_nonneg` `star_star` `StarMul.star_mul` `norm_star` `CStarRing.to_normedStarGroup` `norm_star_mul_mul_self_of_nonneg`
`norm_nnrpow` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `NNReal.instPartialOrder` `NNReal.instZero` `Preorder.toLE` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing`	`Norm.norm` `NonUnitalNormedRing.toNorm` `NNReal` `instPowNNReal` `NonUnitalNormedRing.toNonUnitalRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedSpace.toModule` `Real` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus` `IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `StarRing.toStarAddMonoid` `Real.instCommSemiring` `Real.instNontrivial` `instStarRingReal` `Real.metricSpace` `IsTopologicalRing.toIsTopologicalSemiring` `MetricSpace.toPseudoMetricSpace` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `instIsTopologicalRingReal` `instContinuousStarReal` `NonUnitalNormedRing.toMetricSpace` `Real.instPow` `NNReal.toReal`	—	`Real.instNontrivial` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus` `nnnorm_nnrpow`
`norm_rpow` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	`Norm.norm` `NormedRing.toNorm` `Real` `instPowReal` `NormedRing.toRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedAlgebra.toAlgebra` `Real.normedField` `IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus` `IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarRing.toStarAddMonoid` `Real.instCommSemiring` `instStarRingReal` `Real.metricSpace` `IsTopologicalRing.toIsTopologicalSemiring` `MetricSpace.toPseudoMetricSpace` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `instIsTopologicalRingReal` `instContinuousStarReal` `NormedRing.toMetricSpace` `Real.instPow`	—	`IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus` `nnnorm_rpow`
`norm_sqrt` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing`	`Norm.norm` `NonUnitalNormedRing.toNorm` `sqrt` `NonUnitalNormedRing.toNonUnitalRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedSpace.toModule` `Real` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus` `IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `StarRing.toStarAddMonoid` `Real.instCommSemiring` `Real.instNontrivial` `instStarRingReal` `Real.metricSpace` `IsTopologicalRing.toIsTopologicalSemiring` `MetricSpace.toPseudoMetricSpace` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `instIsTopologicalRingReal` `instContinuousStarReal` `NonUnitalNormedRing.toMetricSpace` `Real.sqrt`	—	`Real.instNontrivial` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus` `Real.coe_sqrt` `nnnorm_sqrt`
`norm_star_mul_mul_self_of_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing`	`Norm.norm` `NonUnitalNormedRing.toNorm` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `Real` `Monoid.toPow` `Real.instMonoid` `sqrt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup`	—	`Real.instNontrivial` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `sq` `CStarRing.norm_star_mul_self` `StarMul.star_mul` `LE.le.star_eq` `sqrt_nonneg` `mul_assoc` `sqrt_mul_sqrt_self` `IsTopologicalRing.toIsSemitopologicalRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`

CFC.IsSelfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`norm_mul_mul_self_of_nonneg` 📖	mathematical	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `StarRing.toStarAddMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`Norm.norm` `NonUnitalNormedRing.toNorm` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `Real` `Monoid.toPow` `Real.instMonoid` `CFC.sqrt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup`	—	`Real.instNontrivial` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `IsSelfAdjoint.star_eq` `CFC.norm_star_mul_mul_self_of_nonneg`
`norm_mul_mul_self_of_nonneg'` 📖	mathematical	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `StarRing.toStarAddMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`Norm.norm` `NonUnitalNormedRing.toNorm` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `Real` `Monoid.toPow` `Real.instMonoid` `CFC.sqrt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup`	—	`Real.instNontrivial` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `IsSelfAdjoint.star_eq` `CFC.norm_mul_mul_star_self_of_nonneg`

---

← Back to Index