Abs

📁 Source: Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Abs.lean

Statistics

Metric	Count
Definitions abs	1
Theorems abs_add_self, abs_algebraMap, abs_algebraMap_nnreal, abs_eq_cfc_norm, abs_eq_cfcₙ_coe_norm, abs_eq_cfcₙ_norm, abs_eq_zero_iff, abs_intCast, abs_mul_abs, abs_mul_self, abs_natCast, abs_neg, abs_nnrpow, abs_nnrpow_two, abs_nnrpow_two_mul, abs_nonneg, abs_ofNat, abs_of_nonneg, abs_of_nonpos, abs_one, abs_smul, abs_smul_nonneg, abs_sq, abs_star, abs_sub_self, abs_zero, cfcAbs_cfcAbs, commute_abs_self, continuous_abs, norm_abs, posPart_add_negPart, quasispectrum_abs, spectrum_abs, cfcAbs_cfcAbs, cfcAbs_left, cfcAbs_mul_eq, cfcAbs_right, cfc_comp_norm, cfcₙ_comp_norm, cfcₙ_norm_nonneg, cfcₙ_norm_sq_nonneg	41
Total	42

CFC

Definitions

Name	Category	Theorems
abs 📖	CompOp	40 math math: abs_smul_nonneg, abs_add_self, abs_eq_cfc_norm, Matrix.IsHermitian.det_abs, abs_eq_cfcₙ_coe_norm, abs_nnrpow_two, cfcAbs_cfcAbs, Commute.cfcAbs_cfcAbs, abs_nonneg, abs_zero, abs_nnrpow, cfcₙ_comp_norm, abs_neg, continuous_abs, abs_of_nonpos, abs_natCast, abs_of_nonneg, abs_nnrpow_two_mul, abs_star, abs_algebraMap, Commute.cfcAbs_right, Commute.cfcAbs_mul_eq, posPart_add_negPart, abs_mul_self, abs_ofNat, abs_algebraMap_nnreal, commute_abs_self, cfc_comp_norm, abs_intCast, quasispectrum_abs, spectrum_abs, norm_abs, Commute.cfcAbs_left, abs_eq_cfcₙ_norm, abs_sq, abs_one, abs_mul_abs, abs_smul, abs_sub_self, abs_eq_zero_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_add_self 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib abs AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup PosPart.posPart CStarAlgebra.instPosPart	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal two_smul add_add_sub_cancel posPart_add_negPart posPart_sub_negPart
abs_algebraMap 📖	mathematical	—	abs Ring.toNonUnitalRing Algebra.toModule Real Real.instCommSemiring Ring.toSemiring Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid Field.toSemifield Real.instField instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal Real.instCompleteSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.instFunLike algebraMap Norm.norm NormedField.toNorm	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital Real.instCompleteSpace abs.congr_simp Algebra.algebraMap_eq_smul_one abs_smul abs_one
abs_algebraMap_nnreal 📖	mathematical	—	abs Ring.toNonUnitalRing Algebra.toModule Real Real.instCommSemiring Ring.toSemiring Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid Field.toSemifield Real.instField instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal Real.instCompleteSpace DFunLike.coe RingHom NNReal Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringNNReal RingHom.instFunLike algebraMap NNReal.instAlgebraOfReal	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital Real.instCompleteSpace abs.congr_simp Algebra.algebraMap_eq_smul_one abs_smul_nonneg IsScalarTower.left abs_one
abs_eq_cfc_norm 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid	abs Ring.toNonUnitalRing Algebra.toModule Real Real.instCommSemiring Ring.toSemiring Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital Field.toSemifield Real.instField instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal Real.instCompleteSpace cfc Norm.norm Real.norm	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital Real.instCompleteSpace Real.instNontrivial abs_eq_cfcₙ_norm IsDomain.toNontrivial instIsDomain cfcₙ_eq_cfc RCLike.uniqueNonUnitalContinuousFunctionalCalculus ContinuousOn.norm continuousOn_id' norm_zero
abs_eq_cfcₙ_coe_norm 📖	mathematical	—	abs cfcₙ Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar RCLike.ofReal Norm.norm NormedField.toNorm	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar Real.instNontrivial instIsTopologicalRingReal instContinuousStarReal abs.eq_1 sqrt_eq_iff cfcₙ_norm_nonneg cfcₙ_mul Continuous.comp_continuousOn' continuous_algebraMap IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousOn.norm continuousOn_id' norm_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass cfcₙ_id' cfcₙ_star ContinuousOn.star star_zero cfcₙ.congr_simp RCLike.conj_mul sq
abs_eq_cfcₙ_norm 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid	abs cfcₙ Real Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal Norm.norm Real.norm	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal abs.eq_1 IsSelfAdjoint.star_eq sqrt_eq_real_sqrt IsSelfAdjoint.mul_self_nonneg cfcₙ_id' cfcₙ_mul continuousOn_id' cfcₙ_comp' RCLike.uniqueNonUnitalContinuousFunctionalCalculus ContinuousOn.sqrt Real.sqrt_zero ContinuousOn.fun_mul IsTopologicalSemiring.toContinuousMul MulZeroClass.mul_zero cfcₙ.congr_simp Real.sqrt_sq_eq_abs
abs_eq_zero_iff 📖	mathematical	—	abs NonUnitalNormedRing.toNonUnitalRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal abs.eq_1 sqrt_eq_zero_iff NonUnitalSeminormedRing.toIsTopologicalRing TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CStarRing.star_mul_self_eq_zero_iff
abs_intCast 📖	mathematical	—	abs Ring.toNonUnitalRing Algebra.toModule Real Real.instCommSemiring Ring.toSemiring Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid Field.toSemifield Real.instField instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal Real.instCompleteSpace AddGroupWithOne.toIntCast Ring.toAddGroupWithOne abs instLatticeInt Int.instAddGroup	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital Real.instCompleteSpace abs.congr_simp Int.cast_natCast abs_natCast Nat.abs_cast IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing Int.cast_negSucc abs_neg
abs_mul_abs 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing abs Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal sqrt_mul_sqrt_self star_mul_self_nonneg
abs_mul_self 📖	mathematical	—	abs Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Commute.cfcAbs_mul_eq Commute.refl Commute.symm IsStarNormal.star_comm_self abs_mul_abs
abs_natCast 📖	mathematical	—	abs Ring.toNonUnitalRing Algebra.toModule Real Real.instCommSemiring Ring.toSemiring Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid Field.toSemifield Real.instField instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal Real.instCompleteSpace AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital Real.instCompleteSpace abs.congr_simp map_natCast RingHom.instRingHomClass abs_algebraMap_nnreal
abs_neg 📖	mathematical	—	abs NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal sqrt.congr_simp star_neg mul_neg neg_mul neg_neg
abs_nnrpow 📖	mathematical	—	NNReal instPowNNReal abs Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NNReal.instDiv instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instSemiringNNReal Nat.instAtLeastTwoHAddOfNat	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Nat.instAtLeastTwoHAddOfNat mul_div_left_comm Real.instIsStrictOrderedRing Nonneg.coe_inv Nonneg.coe_div Nonneg.coe_zpow div_self IsStrictOrderedRing.toCharZero NNReal.instIsStrictOrderedRing mul_one
abs_nnrpow_two 📖	mathematical	—	NNReal instPowNNReal abs instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instSemiringNNReal Nat.instAtLeastTwoHAddOfNat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Nat.instAtLeastTwoHAddOfNat nnrpow_two abs_mul_abs
abs_nnrpow_two_mul 📖	mathematical	—	NNReal instPowNNReal abs Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.instAtLeastTwoHAddOfNat NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Nat.instAtLeastTwoHAddOfNat nnrpow_nnrpow abs_nnrpow_two
abs_nonneg 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing abs	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal sqrt_nonneg
abs_ofNat 📖	mathematical	—	abs Ring.toNonUnitalRing Algebra.toModule Real Real.instCommSemiring Ring.toSemiring Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid Field.toSemifield Real.instField instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal Real.instCompleteSpace	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal abs_natCast
abs_of_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	abs	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal abs.eq_1 LE.le.star_eq sqrt_mul_self
abs_of_nonpos 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	abs NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NonUnitalNonAssocRing.toAddCommGroup	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal abs_neg abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsOrderedAddMonoid.toIsOrderedCancelAddMonoid StarOrderedRing.toIsOrderedAddMonoid
abs_one 📖	mathematical	—	abs Ring.toNonUnitalRing Algebra.toModule Real Real.instCommSemiring Ring.toSemiring Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid Field.toSemifield Real.instField instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal Real.instCompleteSpace AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital Real.instCompleteSpace sqrt.congr_simp star_one mul_one sqrt_one
abs_smul 📖	mathematical	—	abs SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Real Real.instMonoid Real.semiring Norm.norm NormedField.toNorm	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal sqrt.congr_simp StarModule.star_smul mul_smul_comm smul_mul_assoc IsScalarTower.left RCLike.real_smul_eq_coe_smul mul_comm RCLike.conj_mul sq RCLike.conj_ofReal CanLift.prf NNReal.canLift norm_nonneg abs.congr_simp abs_smul_nonneg
abs_smul_nonneg 📖	mathematical	—	abs	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal abs.eq_1 sqrt_eq_iff star_mul_self_nonneg smul_nonneg IsOrderedModule.toPosSMulMono instIsOrderedModule NNReal.instStarOrderedRing instStarModuleNNRealOfReal NNReal.instIsScalarTowerOfReal NNReal.smulCommClass_left zero_le NNReal.instCanonicallyOrderedAdd abs_nonneg mul_smul_comm smul_mul_assoc abs_mul_abs StarModule.star_smul TrivialStar.star_trivial instTrivialStarNNReal abs.congr_simp smul_assoc one_smul
abs_sq 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring abs Ring.toNonUnitalRing Algebra.toModule Real Real.instCommSemiring Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid Field.toSemifield Real.instField instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal Real.instCompleteSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Star.star	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital Real.instCompleteSpace sq abs_mul_abs
abs_star 📖	mathematical	—	abs Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal sqrt.congr_simp star_star star_comm_self'
abs_sub_self 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup abs AddMonoid.toNatSMul SubNegMonoid.toAddMonoid NegPart.negPart CStarAlgebra.instNegPart	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal two_smul add_sub_sub_cancel posPart_add_negPart posPart_sub_negPart
abs_zero 📖	mathematical	—	abs MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal sqrt.congr_simp star_zero MulZeroClass.mul_zero sqrt_zero
cfcAbs_cfcAbs 📖	mathematical	—	abs	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal abs_of_nonneg
commute_abs_self 📖	mathematical	—	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing abs	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Commute.cfcAbs_left Commute.refl Commute.symm IsStarNormal.star_comm_self
continuous_abs 📖	mathematical	—	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing abs 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	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal ContinuousOn.comp_continuous NonUnitalIsometricContinuousFunctionalCalculus.toNonUnitalContinuousFunctionalCalculus continuousOn_sqrt Continuous.comp' continuous_mul IsTopologicalSemiring.toContinuousMul NonUnitalSeminormedRing.toIsTopologicalRing Continuous.prodMk Continuous.star continuous_id'
norm_abs 📖	mathematical	—	Norm.norm NonUnitalNormedRing.toNorm abs NonUnitalNormedRing.toNonUnitalRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NormedSpace.toModule Real Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal sq_eq_sq₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg sq CStarRing.norm_star_mul_self LE.le.star_eq abs_nonneg abs_mul_abs NonUnitalSeminormedRing.toIsTopologicalRing TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
posPart_add_negPart 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib PosPart.posPart CStarAlgebra.instPosPart NegPart.negPart CStarAlgebra.instNegPart abs	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal posPart_def negPart_def cfcₙ_add Continuous.continuousOn continuous_posPart instHasSolidNormReal Real.instIsOrderedAddMonoid posPart_zero continuous_negPart negPart_of_nonpos IsOrderedAddMonoid.toAddLeftMono neg_zero abs_eq_cfcₙ_norm cfcₙ_congr posPart_add_negPart covariant_swap_add_of_covariant_add
quasispectrum_abs 📖	mathematical	—	quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField abs Set.image RCLike.ofReal Norm.norm NormedField.toNorm	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar Real.instNontrivial instIsTopologicalRingReal instContinuousStarReal abs_eq_cfcₙ_coe_norm cfcₙ_map_quasispectrum Continuous.comp_continuousOn' continuous_algebraMap IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousOn.norm continuousOn_id' norm_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
spectrum_abs 📖	mathematical	—	spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField abs Ring.toNonUnitalRing Algebra.toModule Real Real.instCommSemiring Ring.toSemiring Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid Real.instField instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal Real.instCompleteSpace Set.image RCLike.ofReal Norm.norm NormedField.toNorm	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar instIsTopologicalRingReal instContinuousStarReal Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital Real.instCompleteSpace IsLocalRing.toNontrivial Field.instIsLocalRing RCLike.toCompleteSpace abs_eq_cfcₙ_coe_norm IsDomain.toNontrivial instIsDomain cfcₙ_eq_cfc RCLike.uniqueNonUnitalContinuousFunctionalCalculus Continuous.comp_continuousOn' continuous_algebraMap IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousOn.norm continuousOn_id' norm_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass cfc_map_spectrum

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cfcAbs_cfcAbs 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	CFC.abs	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal symm NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus cfcₙ_nnreal star_left
cfcAbs_left 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	CFC.abs	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal cfcₙ_nnreal star_left
cfcAbs_mul_eq 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	CFC.abs	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal cfcAbs_cfcAbs CFC.abs.eq_1 CFC.sqrt_eq_iff star_mul_self_nonneg mul_nonneg CFC.abs_nonneg eq mul_mul_mul_comm CFC.abs_mul_abs StarMul.star_mul symm star_left
cfcAbs_right 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	CFC.abs	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal symm cfcAbs_left

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cfc_comp_norm 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Set.image RCLike.ofReal Norm.norm NormedField.toNorm spectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField	cfc RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar CFC.abs Ring.toNonUnitalRing Algebra.toModule Real Real.instCommSemiring Ring.toSemiring Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid Real.instField instStarRingReal Real.metricSpace Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal Real.instCompleteSpace	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar instIsTopologicalRingReal instContinuousStarReal Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital Real.instCompleteSpace IsLocalRing.toNontrivial Field.instIsLocalRing RCLike.toCompleteSpace CFC.abs_eq_cfcₙ_coe_norm IsDomain.toNontrivial instIsDomain cfcₙ_eq_cfc RCLike.uniqueNonUnitalContinuousFunctionalCalculus Continuous.comp_continuousOn' continuous_algebraMap IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousOn.norm continuousOn_id' norm_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass cfc_comp' RCLike.instContinuousMapUniqueHom
cfcₙ_comp_norm 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Set.image RCLike.ofReal Norm.norm NormedField.toNorm quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField	cfcₙ IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar CFC.abs	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar Real.instNontrivial instIsTopologicalRingReal instContinuousStarReal em cfcₙ_comp' RCLike.uniqueNonUnitalContinuousFunctionalCalculus Continuous.comp_continuousOn' continuous_algebraMap IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousOn.norm continuousOn_id' norm_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass CFC.abs_eq_cfcₙ_coe_norm cfcₙ_apply_of_not_map_zero
cfcₙ_norm_nonneg 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing cfcₙ Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar RCLike.ofReal Norm.norm NormedField.toNorm	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar cfcₙ_nonneg RCLike.toStarOrderedRing NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass
cfcₙ_norm_sq_nonneg 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing cfcₙ Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing RCLike.toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	—	IsLocalRing.toNontrivial Field.instIsLocalRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar cfcₙ_nonneg RCLike.toStarOrderedRing NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass star_mul_self_nonneg

---

← Back to Index