Unitization

📁 Source: Mathlib/Analysis/Normed/Algebra/Unitization.lean

Statistics

Metric	Count
Definitions Unitization, instBornology, instMetricSpace, instNormedAlgebra, instNormedRing, instUniformSpace, normedAlgebraAux, normedRingAux, splitMul, uniformEquivProd	10
Theorems antilipschitzWith_addEquiv, cobounded_eq_aux, continuous_inr, dist_inr, instCompleteSpace, instNormOneClass, isUniformEmbedding_addEquiv, isometry_inr, lipschitzWith_addEquiv, nndist_inr, nnnorm_def, nnnorm_eq_sup, nnnorm_inr, norm_def, norm_eq_sup, norm_inr, splitMul_apply, splitMul_injective, splitMul_injective_of_clm_mul_injective, uniformity_eq_aux	20
Total	30

Unitization

Definitions

Name	Category	Theorems
instBornology 📖	CompOp	—
instMetricSpace 📖	CompOp	1 math math: isometry_inr
instNormedAlgebra 📖	CompOp	—
instNormedRing 📖	CompOp	6 math math: dist_inr, instCStarRing, instNormOneClass, nndist_inr, norm_inr, nnnorm_inr
instUniformSpace 📖	CompOp	8 math math: real_cfcₙ_eq_cfc_inr, isClosedEmbedding_cfcₙAux, nnreal_cfcₙ_eq_cfc_inr, isUniformEmbedding_addEquiv, complex_cfcₙ_eq_cfc_inr, instCompleteSpace, continuous_inr, cfcₙ_eq_cfc_inr
normedAlgebraAux 📖	CompOp	—
normedRingAux 📖	CompOp	8 math math: nnnorm_def, cobounded_eq_aux, norm_eq_sup, norm_def, nnnorm_eq_sup, antilipschitzWith_addEquiv, uniformity_eq_aux, lipschitzWith_addEquiv
splitMul 📖	CompOp	6 math math: splitMul_apply, nnnorm_def, splitMul_injective_of_clm_mul_injective, norm_def, norm_splitMul_snd_sq, splitMul_injective
uniformEquivProd 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antilipschitzWith_addEquiv 📖	mathematical	—	AntilipschitzWith Unitization EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedRing.toMetricSpace normedRingAux Prod.pseudoEMetricSpaceMax NormedField.toMetricSpace NontriviallyNormedField.toNormedField NonUnitalNormedRing.toMetricSpace NNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instSemiringNNReal Nat.instAtLeastTwoHAddOfNat DFunLike.coe AddEquiv instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing Prod.instAdd EquivLike.toFunLike AddEquiv.instEquivLike addEquiv	—	AddMonoidHomClass.antilipschitz_of_bound AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass Nat.instAtLeastTwoHAddOfNat IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing smulCommClass_self IsScalarTower.left UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup norm_eq_sup Prod.norm_def NNReal.coe_two max_le mul_max_of_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing zero_le_two Real.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid le_max_of_le_left LE.le.trans_eq le_add_of_nonneg_left covariant_swap_add_of_covariant_add norm_nonneg two_mul Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim ContinuousLinearMap.opNorm_subsingleton RingHomIsometric.ids norm_of_subsingleton sup_of_le_left IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instNontrivial norm_add_le norm_algebraMap' ContinuousLinearMap.normOneClass EMetric.instNontrivialTopologyOfNontrivial AddMonoidHomClass.isometry_iff_norm DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass ContinuousLinearMap.isometry_mul add_le_add le_max_left le_max_right
cobounded_eq_aux 📖	mathematical	—	Bornology.cobounded Unitization Bornology.induced Prod.instBornology PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing DFunLike.coe AddEquiv instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing Prod.instAdd EquivLike.toFunLike AddEquiv.instEquivLike addEquiv NormedRing.toSeminormedRing normedRingAux	—	le_antisymm LipschitzWith.comap_cobounded_le Nat.instAtLeastTwoHAddOfNat lipschitzWith_addEquiv Filter.Tendsto.le_comap AntilipschitzWith.tendsto_cobounded antilipschitzWith_addEquiv
continuous_inr 📖	mathematical	—	Continuous Unitization UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing instUniformSpace inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField	—	Isometry.continuous isometry_inr
dist_inr 📖	mathematical	—	Dist.dist Unitization PseudoMetricSpace.toDist SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing instNormedRing inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing	—	Isometry.dist_eq isometry_inr
instCompleteSpace 📖	mathematical	—	CompleteSpace Unitization instUniformSpace	—	UniformEquiv.completeSpace_iff CompleteSpace.prod
instNormOneClass 📖	mathematical	—	NormOneClass Unitization NormedRing.toNorm instNormedRing instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing smulCommClass_self IsScalarTower.left UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup norm_eq_sup NormOneClass.norm_one NormedDivisionRing.to_normOneClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass add_zero RingHomIsometric.ids ContinuousLinearMap.opNorm_le_bound zero_le_one Real.instZeroLEOneClass one_mul
isUniformEmbedding_addEquiv 📖	mathematical	—	IsUniformEmbedding Unitization instUniformSpace instUniformSpaceProd PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing DFunLike.coe AddEquiv instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing Prod.instAdd EquivLike.toFunLike AddEquiv.instEquivLike addEquiv	—	AddEquiv.injective
isometry_inr 📖	mathematical	—	Isometry Unitization EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NonUnitalNormedRing.toMetricSpace instMetricSpace inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField	—	AddMonoidHomClass.isometry_of_norm DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass NonUnitalAlgHom.instNonUnitalAlgSemiHomClass norm_inr
lipschitzWith_addEquiv 📖	mathematical	—	LipschitzWith Unitization EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedRing.toMetricSpace normedRingAux Prod.pseudoEMetricSpaceMax NormedField.toMetricSpace NontriviallyNormedField.toNormedField NonUnitalNormedRing.toMetricSpace NNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instSemiringNNReal Nat.instAtLeastTwoHAddOfNat DFunLike.coe AddEquiv instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing Prod.instAdd EquivLike.toFunLike AddEquiv.instEquivLike addEquiv	—	Nat.instAtLeastTwoHAddOfNat Real.toNNReal_ofNat AddMonoidHomClass.lipschitz_of_bound AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing smulCommClass_self IsScalarTower.left UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup norm_eq_sup Prod.norm_def max_le mul_max_of_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing zero_le_two Real.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid le_max_of_le_left LE.le.trans_eq le_add_of_nonneg_left covariant_swap_add_of_covariant_add norm_nonneg two_mul Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim norm_of_subsingleton ContinuousLinearMap.opNorm_subsingleton RingHomIsometric.ids sup_of_le_left IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instNontrivial Isometry.norm_map_of_map_zero ContinuousLinearMap.isometry_mul map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass add_comm norm_algebraMap' ContinuousLinearMap.normOneClass EMetric.instNontrivialTopologyOfNontrivial norm_le_add_norm_add add_le_add le_sup_right le_sup_left
nndist_inr 📖	mathematical	—	NNDist.nndist Unitization PseudoMetricSpace.toNNDist SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing instNormedRing inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing	—	Isometry.nndist_eq isometry_inr
nnnorm_def 📖	mathematical	—	NNNorm.nnnorm Unitization SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing normedRingAux ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedSpace.toModule Prod.seminormedAddGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toSeminormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing DFunLike.coe AlgHom Semifield.toCommSemiring instSemiring NonUnitalRing.toNonUnitalSemiring NonUnitalNormedRing.toNonUnitalRing Prod.instSemiring ContinuousLinearMap.semiring IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing instAlgebra Algebra.id Module.toDistribMulAction CommSemiring.toSemiring IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Prod.algebra ContinuousLinearMap.algebra SeminormedAddCommGroup.toAddCommGroup smulCommClass_self CommRing.toCommMonoid Field.toCommRing CommMonoid.toMonoid Ring.toSemiring CommRing.toRing Algebra.toSMul UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul AddCommGroup.toAddCommMonoid IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup AlgHom.funLike splitMul	—	—
nnnorm_eq_sup 📖	mathematical	—	NNNorm.nnnorm Unitization SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing normedRingAux NNReal NNReal.instMax NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField fst ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedSpace.toModule ContinuousLinearMap.toSeminormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalSeminormedRing.toNonUnitalRing ContinuousLinearMap.add IsTopologicalSemiring.toContinuousAdd NonUnitalNormedRing.toNonUnitalRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing DFunLike.coe RingHom CommSemiring.toSemiring Semifield.toCommSemiring ContinuousLinearMap.semiring RingHom.instFunLike algebraMap ContinuousLinearMap.algebra SeminormedAddCommGroup.toAddCommGroup smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul AddCommGroup.toAddCommMonoid IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.topologicalSpace ContinuousLinearMap.addCommMonoid ContinuousLinearMap.module ContinuousLinearMap.funLike ContinuousLinearMap.mul snd	—	NNReal.eq RingHomIsometric.ids IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing smulCommClass_self IsScalarTower.left UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup norm_eq_sup
nnnorm_inr 📖	mathematical	—	NNNorm.nnnorm Unitization SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing instNormedRing inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField	—	NNReal.eq norm_inr
norm_def 📖	mathematical	—	Norm.norm Unitization NormedRing.toNorm normedRingAux ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup Prod.toNorm NormedField.toNorm ContinuousLinearMap.hasOpNorm DFunLike.coe AlgHom Semifield.toCommSemiring instSemiring NonUnitalRing.toNonUnitalSemiring NonUnitalNormedRing.toNonUnitalRing Prod.instSemiring ContinuousLinearMap.semiring IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing instAlgebra Algebra.id Module.toDistribMulAction CommSemiring.toSemiring IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Prod.algebra ContinuousLinearMap.algebra SeminormedAddCommGroup.toAddCommGroup smulCommClass_self CommRing.toCommMonoid Field.toCommRing CommMonoid.toMonoid Ring.toSemiring CommRing.toRing Algebra.toSMul UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul AddCommGroup.toAddCommMonoid IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup AlgHom.funLike splitMul	—	—
norm_eq_sup 📖	mathematical	—	Norm.norm Unitization NormedRing.toNorm normedRingAux Real Real.instMax NormedField.toNorm NontriviallyNormedField.toNormedField fst ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup ContinuousLinearMap.hasOpNorm NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalSeminormedRing.toNonUnitalRing ContinuousLinearMap.add IsTopologicalSemiring.toContinuousAdd NonUnitalNormedRing.toNonUnitalRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing DFunLike.coe RingHom CommSemiring.toSemiring Semifield.toCommSemiring ContinuousLinearMap.semiring RingHom.instFunLike algebraMap ContinuousLinearMap.algebra SeminormedAddCommGroup.toAddCommGroup smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul AddCommGroup.toAddCommMonoid IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.topologicalSpace ContinuousLinearMap.addCommMonoid ContinuousLinearMap.module ContinuousLinearMap.funLike ContinuousLinearMap.mul snd	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing smulCommClass_self IsScalarTower.left UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup norm_def splitMul_apply Prod.norm_def
norm_inr 📖	mathematical	—	Norm.norm Unitization NormedRing.toNorm instNormedRing inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NonUnitalNormedRing.toNorm	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing smulCommClass_self IsScalarTower.left UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup norm_eq_sup norm_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass zero_add RingHomIsometric.ids ContinuousLinearMap.opNorm_mul_apply sup_of_le_right
splitMul_apply 📖	mathematical	—	DFunLike.coe AlgHom Unitization ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup Semifield.toCommSemiring instSemiring NonUnitalRing.toNonUnitalSemiring NonUnitalNormedRing.toNonUnitalRing Prod.instSemiring ContinuousLinearMap.semiring IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing instAlgebra Algebra.id Module.toDistribMulAction CommSemiring.toSemiring IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Prod.algebra ContinuousLinearMap.algebra SeminormedAddCommGroup.toAddCommGroup smulCommClass_self CommRing.toCommMonoid Field.toCommRing CommMonoid.toMonoid Ring.toSemiring CommRing.toRing Algebra.toSMul UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul AddCommGroup.toAddCommMonoid IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup AlgHom.funLike splitMul fst NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSeminormedRing.toNonUnitalRing ContinuousLinearMap.add RingHom RingHom.instFunLike algebraMap ContinuousLinearMap.topologicalSpace ContinuousLinearMap.addCommMonoid ContinuousLinearMap.module ContinuousLinearMap.funLike ContinuousLinearMap.mul snd	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing smulCommClass_self IsScalarTower.left UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup add_zero
splitMul_injective 📖	mathematical	—	Unitization ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup DFunLike.coe AlgHom Semifield.toCommSemiring instSemiring NonUnitalRing.toNonUnitalSemiring NonUnitalNormedRing.toNonUnitalRing Prod.instSemiring ContinuousLinearMap.semiring IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing instAlgebra Algebra.id Module.toDistribMulAction CommSemiring.toSemiring IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Prod.algebra ContinuousLinearMap.algebra SeminormedAddCommGroup.toAddCommGroup smulCommClass_self CommRing.toCommMonoid Field.toCommRing CommMonoid.toMonoid Ring.toSemiring CommRing.toRing Algebra.toSMul UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul AddCommGroup.toAddCommMonoid IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup AlgHom.funLike splitMul	—	splitMul_injective_of_clm_mul_injective Isometry.injective RingHomIsometric.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.isometry_mul
splitMul_injective_of_clm_mul_injective 📖	mathematical	ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalSeminormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup DFunLike.coe ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toIsBoundedSMul ContinuousLinearMap.funLike ContinuousLinearMap.mul	Unitization ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup AlgHom Semifield.toCommSemiring instSemiring NonUnitalRing.toNonUnitalSemiring NonUnitalNormedRing.toNonUnitalRing Prod.instSemiring ContinuousLinearMap.semiring instAlgebra Algebra.id CommSemiring.toSemiring IsScalarTower.left Prod.algebra ContinuousLinearMap.algebra Algebra.toSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGroup.toAddCommMonoid AlgHom.funLike splitMul	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsScalarTower.left RingHomIsometric.ids injective_iff_map_eq_zero DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass ind splitMul_apply map_zero AddMonoidHomClass.toZeroHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass add_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass zero_add map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass inr_zero
uniformity_eq_aux 📖	mathematical	—	uniformity Unitization UniformSpace.comap DFunLike.coe AddEquiv instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing Prod.instAdd EquivLike.toFunLike AddEquiv.instEquivLike addEquiv instUniformSpaceProd PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toSeminormedRing normedRingAux	—	AntilipschitzWith.isUniformInducing Nat.instAtLeastTwoHAddOfNat antilipschitzWith_addEquiv LipschitzWith.uniformContinuous lipschitzWith_addEquiv IsUniformInducing.comap_uniformity

(root)

Definitions

Name	Category	Theorems
Unitization 📖	CompOp	159 math math: CStarAlgebra.preimage_inr_Icc_zero_one, Unitization.inr_neg, Unitization.isometry_inr, Unitization.inrNonUnitalAlgHom_toFun, CStarAlgebra.inr_mem_Icc_iff_norm_le, quasispectrumRestricts_iff_spectrumRestricts_inr', Unitization.real_cfcₙ_eq_cfc_inr, isClosedEmbedding_cfcₙAux, Unitization.splitMul_apply, Unitization.inr_sub, Unitization.algHom_ext'_iff, WithLp.instCompleteSpace, Unitization.starAlgHom_ext_iff, Unitization.inl_mul_inr, NonUnitalStarSubalgebra.unitizationStarAlgEquiv_apply_coe, Unitization.inl_injective, Unitization.isIdempotentElem_inr_iff, Unitization.isQuasiregular_inr_iff, Unitization.starLift_symm_apply_apply, Unitization.starLift_apply_apply, Unitization.inl_one, Unitization.instSMulCommClass, Unitization.fst_zero, Unitization.inr_star, Unitization.inr_le_iff, Unitization.nnnorm_def, Unitization.dist_inr, Unitization.instStarOrderedRing, WithLp.unitization_algebraMap, Unitization.inl_mul, NonUnitalSubalgebra.unitization_injective, Unitization.lift_symm_apply_apply, Unitization.snd_mul, NonUnitalStarSubalgebra.unitization_range, NonUnitalSubalgebra.unitization_range, Unitization.quasispectrum_inr_eq, Unitization.fst_mul, NonUnitalSubsemiring.unitization_apply, NonUnitalSubring.unitization_apply, Unitization.cobounded_eq_aux, Unitization.inl_zero, Unitization.zero_mem_spectrum_inr, Unitization.splitMul_injective_of_clm_mul_injective, cfcₙAux_id, Unitization.starMap_injective, IsSelfAdjoint.inr, NonUnitalAlgHom.toAlgHom_zero, Unitization.starMap_id, Unitization.inr_mul, Unitization.instCanLift, Unitization.starLift_range, Unitization.inl_star, Unitization.inr_smul, Unitization.inrNonUnitalStarAlgHom_apply, Unitization.starMap_inl, Unitization.inl_mul_inl, Unitization.starMap_inr, Unitization.fst_add, Unitization.algebraMap_eq_inl, Unitization.sndHom_apply, Unitization.val_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, Unitization.isSelfAdjoint_inr, Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, NonUnitalStarSubalgebra.unitization_injective, NonUnitalStarSubalgebra.unitization_apply, Unitization.starMap_surjective, Unitization.inr_injective, Unitization.norm_eq_sup, inr_comp_cfcₙHom_eq_cfcₙAux, NonUnitalSubalgebra.unitizationAlgEquiv_apply_coe, Unitization.inrHom_apply, Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_apply, Unitization.mem_spectrum_inr_of_not_isUnit, Unitization.lift_range, Unitization.algebraMap_eq_inlRingHom_comp, WithLp.unitization_nnnorm_inr, NonUnitalSubalgebra.unitization_apply, Unitization.lift_symm_apply, WithLp.unitization_norm_def, Unitization.inr_add, Unitization.norm_def, Unitization.fst_one, Unitization.instNontrivialRight, WithLp.unitizationAlgEquiv_symm_apply_ofLp, Unitization.inr_mul_inl, spec_cfcₙAux, Unitization.instNontrivialLeft, Unitization.nnreal_cfcₙ_eq_cfc_inr, Unitization.IsIdempotentElem.inr, Unitization.starLift_apply, Unitization.starMap_comp, Unitization.instIsCentralScalar, quasispectrumRestricts_iff_spectrumRestricts_inr, Unitization.instCStarRing, Unitization.fstHom_apply, Unitization.starMap_apply, Unitization.instIsStarNormal, Unitization.inr_zero, NonUnitalSubring.unitization_range, Unitization.snd_one, Unitization.isUniformEmbedding_addEquiv, cfcₙAux_mem_range_inr, NonUnitalAlgHom.toAlgHom_apply, Unitization.nnnorm_eq_sup, Unitization.snd_zero, Unitization.instNormOneClass, Unitization.snd_star, Unitization.quasispectrum_eq_spectrum_inr', Unitization.inrRangeEquiv_apply_coe, Unitization.instStarModule, NonUnitalSubsemiring.unitization_range, Unitization.complex_cfcₙ_eq_cfc_inr, Unitization.inrNonUnitalAlgHom_apply, Unitization.lift_range_le, Unitization.nndist_inr, isQuasiregular_iff_isUnit', Unitization.snd_add, Unitization.norm_splitMul_snd_sq, Unitization.instIsScalarTower, Unitization.antilipschitzWith_addEquiv, Unitization.splitMul_injective, CStarAlgebra.inr_mem_Icc_iff_nnnorm_le, Unitization.snd_neg, Unitization.starLift_range_le, Unitization.inl_neg, WithLp.unitization_mul, Unitization.lift_apply_apply, Unitization.fst_smul, Unitization.uniformity_eq_aux, Unitization.inl_add, Unitization.starLift_symm_apply, Unitization.instCompleteSpace, Unitization.lipschitzWith_addEquiv, Unitization.inl_sub, WithLp.unitizationAlgEquiv_apply, Unitization.algebraMap_eq_inlRingHom, Unitization.val_unitsFstOne_mulEquiv_quasiregular_apply, Unitization.inl_smul, Unitization.quasispectrum_eq_spectrum_inr, Unitization.unitsFstOne_val_val_fst, WithLp.unitization_norm_inr, Unitization.lift_apply, WithLp.unitization_nnnorm_def, Unitization.inrRangeEquiv_symm_apply, Unitization.fst_star, Unitization.inl_fst_add_inr_snd_eq, WithLp.unitization_isometry_inr, Unitization.inlRingHom_apply, Unitization.mem_unitsFstOne, Unitization.fst_neg, Unitization.norm_inr, Unitization.inr_nonneg_iff, Unitization.continuous_inr, Unitization.unitsFstOne_val_inv_val_fst, Unitization.isStarNormal_inr, Unitization.algebraMap_eq_inl_comp, Unitization.nnnorm_inr, Unitization.cfcₙ_eq_cfc_inr, Unitization.snd_smul

---

← Back to Index