Multiplier

📁 Source: Mathlib/Analysis/CStarAlgebra/Multiplier.lean

Statistics

Metric	Count
Definitions DoubleCentralizer, coeHom, instAdd, instAlgebra, instCStarAlgebraComplex, instCoeTC, instInhabited, instIntCast, instModule, instMul, instNatCast, instNeg, instNormedAlgebra, instNormedRing, instNormedSpace, instOne, instPow, instRing, instSMul, instStar, instStarAddMonoid, instStarRing, instSub, instZero, toProd, toProdHom, toProdMulOpposite, toProdMulOppositeHom, «term𝓜(_,_)»»)	29
Theorems add_fst, add_snd, add_toProd, algebraMap_fst, algebraMap_snd, algebraMap_toProd, central, coeHom_apply, coe_eq_algebraMap, coe_fst, coe_snd, ext, ext_iff, instCStarRing, instCompleteSpace, instIsCentralScalar, instIsScalarTower, instSMulCommClass, instStarModule, intCast_fst, intCast_snd, intCast_toProd, isUniformEmbedding_toProdMulOpposite, mul_fst, mul_snd, natCast_fst, natCast_snd, natCast_toProd, neg_fst, neg_snd, neg_toProd, nnnorm_def, nnnorm_def', nnnorm_fst, nnnorm_fst_eq_snd, nnnorm_snd, norm_def, norm_def', norm_fst, norm_fst_eq_snd, norm_snd, one_fst, one_snd, one_toProd, pow_fst, pow_snd, pow_toProd, range_toProd, range_toProdMulOpposite, smul_fst, smul_snd, smul_toProd, star_fst, star_snd, sub_fst, sub_snd, sub_toProd, toProdHom_apply, toProdMulOppositeHom_apply, toProdMulOpposite_injective, zero_fst, zero_snd, zero_toProd	63
Total	92

DoubleCentralizer

Definitions

Name	Category	Theorems
coeHom 📖	CompOp	1 math math: coeHom_apply
instAdd 📖	CompOp	3 math math: add_fst, add_snd, add_toProd
instAlgebra 📖	CompOp	4 math math: algebraMap_snd, algebraMap_toProd, algebraMap_fst, coe_eq_algebraMap
instCStarAlgebraComplex 📖	CompOp	—
instCoeTC 📖	CompOp	—
instInhabited 📖	CompOp	—
instIntCast 📖	CompOp	3 math math: intCast_snd, intCast_fst, intCast_toProd
instModule 📖	CompOp	1 math math: coeHom_apply
instMul 📖	CompOp	2 math math: mul_fst, mul_snd
instNatCast 📖	CompOp	3 math math: natCast_fst, natCast_toProd, natCast_snd
instNeg 📖	CompOp	3 math math: neg_snd, neg_toProd, neg_fst
instNormedAlgebra 📖	CompOp	—
instNormedRing 📖	CompOp	11 math math: nnnorm_def', nnnorm_snd, norm_def', norm_def, nnnorm_def, norm_snd, nnnorm_fst, instCStarRing, norm_fst, isUniformEmbedding_toProdMulOpposite, instCompleteSpace
instNormedSpace 📖	CompOp	—
instOne 📖	CompOp	3 math math: one_snd, one_fst, one_toProd
instPow 📖	CompOp	3 math math: pow_snd, pow_toProd, pow_fst
instRing 📖	CompOp	11 math math: nnnorm_def', norm_def', norm_def, nnnorm_def, algebraMap_snd, algebraMap_toProd, coeHom_apply, algebraMap_fst, coe_eq_algebraMap, toProdHom_apply, toProdMulOppositeHom_apply
instSMul 📖	CompOp	7 math math: instIsScalarTower, smul_toProd, smul_fst, instIsCentralScalar, instStarModule, instSMulCommClass, smul_snd
instStar 📖	CompOp	4 math math: star_snd, star_fst, coeHom_apply, instStarModule
instStarAddMonoid 📖	CompOp	—
instStarRing 📖	CompOp	1 math math: instCStarRing
instSub 📖	CompOp	3 math math: sub_toProd, sub_fst, sub_snd
instZero 📖	CompOp	3 math math: zero_snd, zero_fst, zero_toProd
toProd 📖	CompOp	46 math math: star_snd, intCast_snd, natCast_fst, zero_snd, ext_iff, pow_snd, nnnorm_snd, smul_toProd, norm_fst_eq_snd, central, neg_snd, range_toProd, add_fst, smul_fst, star_fst, add_snd, norm_snd, nnnorm_fst, neg_toProd, algebraMap_snd, one_snd, algebraMap_toProd, pow_toProd, zero_fst, sub_toProd, nnnorm_fst_eq_snd, one_fst, sub_fst, pow_fst, algebraMap_fst, mul_fst, zero_toProd, norm_fst, coe_fst, natCast_toProd, one_toProd, natCast_snd, sub_snd, intCast_fst, toProdHom_apply, mul_snd, intCast_toProd, smul_snd, coe_snd, add_toProd, neg_fst
toProdHom 📖	CompOp	3 math math: norm_def, nnnorm_def, toProdHom_apply
toProdMulOpposite 📖	CompOp	4 math math: range_toProdMulOpposite, toProdMulOpposite_injective, isUniformEmbedding_toProdMulOpposite, toProdMulOppositeHom_apply
toProdMulOppositeHom 📖	CompOp	3 math math: nnnorm_def', norm_def', toProdMulOppositeHom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_fst 📖	mathematical	—	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 toProd DoubleCentralizer instAdd ContinuousLinearMap.add IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing	—	—
add_snd 📖	mathematical	—	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 toProd DoubleCentralizer instAdd ContinuousLinearMap.add IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing	—	—
add_toProd 📖	mathematical	—	toProd DoubleCentralizer instAdd 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.instAdd ContinuousLinearMap.add IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing	—	—
algebraMap_fst 📖	mathematical	—	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 toProd DFunLike.coe RingHom DoubleCentralizer CommSemiring.toSemiring Semifield.toCommSemiring Ring.toSemiring instRing RingHom.instFunLike algebraMap instAlgebra ContinuousLinearMap.semiring IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing ContinuousLinearMap.algebra SeminormedAddCommGroup.toAddCommGroup smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction 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	—	—
algebraMap_snd 📖	mathematical	—	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 toProd DFunLike.coe RingHom DoubleCentralizer CommSemiring.toSemiring Semifield.toCommSemiring Ring.toSemiring instRing RingHom.instFunLike algebraMap instAlgebra ContinuousLinearMap.semiring IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing ContinuousLinearMap.algebra SeminormedAddCommGroup.toAddCommGroup smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction 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	—	—
algebraMap_toProd 📖	mathematical	—	toProd DFunLike.coe RingHom DoubleCentralizer Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Ring.toSemiring instRing RingHom.instFunLike algebraMap instAlgebra ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.id UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup Prod.instSemiring ContinuousLinearMap.semiring IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing Prod.algebra ContinuousLinearMap.algebra SeminormedAddCommGroup.toAddCommGroup smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction 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	—	—
central 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing DFunLike.coe 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 ContinuousLinearMap.funLike toProd	—	—
coeHom_apply 📖	mathematical	—	DFunLike.coe NonUnitalStarAlgHom DoubleCentralizer MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRing instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toIsBoundedSMul instStar NonUnitalStarAlgHom.instFunLike coeHom coe	—	smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
coe_eq_algebraMap 📖	mathematical	—	coe NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace Algebra.to_smulCommClass Semifield.toCommSemiring Field.toSemifield NormedField.toField CommSemiring.toSemiring Algebra.id IsScalarTower.right DFunLike.coe RingHom DoubleCentralizer Semiring.toNonAssocSemiring Ring.toSemiring instRing RingHom.instFunLike algebraMap instAlgebra	—	Algebra.to_smulCommClass IsScalarTower.right ext ContinuousLinearMap.ext mul_comm
coe_fst 📖	mathematical	—	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 toProd coe DFunLike.coe NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalSeminormedRing.toNonUnitalRing 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	—	—
coe_snd 📖	mathematical	—	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 toProd coe DFunLike.coe SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup 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 NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul ContinuousLinearMap.funLike ContinuousLinearMap.flip RingHomIsometric.ids ContinuousLinearMap.mul	—	—
ext 📖	—	toProd	—	—	—
ext_iff 📖	mathematical	—	toProd	—	ext
instCStarRing 📖	mathematical	—	CStarRing DoubleCentralizer DenselyNormedField.toNontriviallyNormedField NormedRing.toNonUnitalNormedRing instNormedRing instStarRing CStarRing.to_normedStarGroup	—	CStarRing.to_normedStarGroup le_of_eq Metric.nonempty_closedBall zero_le_one Real.instZeroLEOneClass central RingHomIsometric.ids nnnorm_mul_le nnnorm_star mul_le_mul' NNReal.mulLeftMono covariant_swap_mul_of_covariant_mul ContinuousLinearMap.le_opNorm_of_le Eq.trans_le nnnorm_fst mul_one nnnorm_snd Set.image_congr SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.opNNNorm_mul_apply CStarRing.instRegularNormedAlgebra csSup_eq_of_forall_le_of_forall_lt_exists_gt Set.Nonempty.image csSup_le mem_closedBall_zero_iff NNReal.sqrt_lt_sqrt NNReal.sqrt_mul_self exists_lt_of_lt_csSup lt_csSup_of_lt star_star CStarRing.nnnorm_star_mul_self NNReal.sq_sqrt pow_lt_pow_left₀ LinearOrderedCommMonoidWithZero.toPosMulStrictMono IsOrderedRing.toMulPosMono NNReal.instIsOrderedRing zero_le' two_ne_zero
instCompleteSpace 📖	mathematical	—	CompleteSpace DoubleCentralizer PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing instNormedRing	—	SeminormedAddCommGroup.to_isUniformAddGroup completeSpace_iff_isComplete_range IsUniformEmbedding.isUniformInducing isUniformEmbedding_toProdMulOpposite IsClosed.isComplete CompleteSpace.prod ContinuousLinearMap.instCompleteSpace SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul FrechetUrysohnSpace.to_sequentialSpace FirstCountableTopology.frechetUrysohnSpace TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace CompleteSpace.mulOpposite range_toProdMulOpposite Set.setOf_forall isClosed_iInter isClosed_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Continuous.comp' Continuous.fun_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing Continuous.fst continuous_id' Continuous.snd Continuous.prodMk continuous_const Continuous.eval_const ContinuousLinearMap.instContinuousEvalConst MulOpposite.continuous_unop
instIsCentralScalar 📖	mathematical	—	IsCentralScalar DoubleCentralizer instSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup MulOpposite MulOpposite.instMonoid MulOpposite.instSemiring SMulCommClass.op_right SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup ContinuousConstSMul.op IsScalarTower.op_left NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing SMulCommClass.op_left	—	SMulCommClass.op_right ContinuousConstSMul.op IsScalarTower.op_left SMulCommClass.op_left ext IsCentralScalar.op_smul_eq_smul Prod.isCentralScalar ContinuousLinearMap.isCentralScalar
instIsScalarTower 📖	mathematical	—	IsScalarTower DoubleCentralizer instSMul	—	ext smul_assoc Prod.isScalarTower ContinuousLinearMap.isScalarTower
instSMulCommClass 📖	mathematical	—	SMulCommClass DoubleCentralizer instSMul	—	ext SMulCommClass.smul_comm Prod.smulCommClass ContinuousLinearMap.smulCommClass
instStarModule 📖	mathematical	—	StarModule DoubleCentralizer InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField StarRing.toStarAddMonoid instStar instSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing NormedSpace.toIsBoundedSMul	—	smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ext ContinuousLinearMap.ext StarModule.star_smul
intCast_fst 📖	mathematical	—	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 toProd DoubleCentralizer instIntCast AddGroupWithOne.toIntCast Ring.toAddGroupWithOne ContinuousLinearMap.ring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup	—	—
intCast_snd 📖	mathematical	—	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 toProd DoubleCentralizer instIntCast AddGroupWithOne.toIntCast Ring.toAddGroupWithOne ContinuousLinearMap.ring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup	—	—
intCast_toProd 📖	mathematical	—	toProd DoubleCentralizer instIntCast 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 AddGroupWithOne.toIntCast Prod.instAddGroupWithOne Ring.toAddGroupWithOne ContinuousLinearMap.ring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup	—	—
isUniformEmbedding_toProdMulOpposite 📖	mathematical	—	IsUniformEmbedding DoubleCentralizer 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 MulOpposite SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing instNormedRing instUniformSpaceProd ContinuousLinearMap.uniformSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.to_isUniformAddGroup instUniformSpaceMulOpposite toProdMulOpposite	—	isUniformEmbedding_comap SeminormedAddCommGroup.to_isUniformAddGroup toProdMulOpposite_injective
mul_fst 📖	mathematical	—	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 toProd DoubleCentralizer instMul ContinuousLinearMap.instMul	—	—
mul_snd 📖	mathematical	—	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 toProd DoubleCentralizer instMul ContinuousLinearMap.instMul	—	—
natCast_fst 📖	mathematical	—	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 toProd DoubleCentralizer instNatCast ContinuousLinearMap.instNatCast IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing	—	—
natCast_snd 📖	mathematical	—	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 toProd DoubleCentralizer instNatCast ContinuousLinearMap.instNatCast IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing	—	—
natCast_toProd 📖	mathematical	—	toProd DoubleCentralizer instNatCast 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 AddMonoidWithOne.toNatCast Prod.instAddMonoidWithOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne ContinuousLinearMap.ring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup	—	—
neg_fst 📖	mathematical	—	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 toProd DoubleCentralizer instNeg ContinuousLinearMap.neg NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup	—	—
neg_snd 📖	mathematical	—	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 toProd DoubleCentralizer instNeg ContinuousLinearMap.neg NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup	—	—
neg_toProd 📖	mathematical	—	toProd DoubleCentralizer instNeg 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.instNeg ContinuousLinearMap.neg NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup	—	—
nnnorm_def 📖	mathematical	—	NNNorm.nnnorm DoubleCentralizer SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing instNormedRing 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 ContinuousLinearMap.toSeminormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instRing Prod.instAddZeroClass ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ContinuousLinearMap.toNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid AddMonoidHom.instFunLike toProdHom	—	—
nnnorm_def' 📖	mathematical	—	NNNorm.nnnorm DoubleCentralizer SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing instNormedRing 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 MulOpposite Prod.seminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulOpposite.instSeminormedAddGroup DFunLike.coe RingHom Ring.toSemiring instRing Prod.instNonAssocSemiring ContinuousLinearMap.semiring IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing MulOpposite.instNonAssocSemiring RingHom.instFunLike toProdMulOppositeHom	—	—
nnnorm_fst 📖	mathematical	—	NNNorm.nnnorm 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 SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing toProd DoubleCentralizer NormedRing.toNonUnitalNormedRing instNormedRing	—	RingHomIsometric.ids norm_fst
nnnorm_fst_eq_snd 📖	mathematical	—	NNNorm.nnnorm 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 SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing toProd	—	RingHomIsometric.ids norm_fst_eq_snd
nnnorm_snd 📖	mathematical	—	NNNorm.nnnorm 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 SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing toProd DoubleCentralizer NormedRing.toNonUnitalNormedRing instNormedRing	—	RingHomIsometric.ids norm_snd
norm_def 📖	mathematical	—	Norm.norm DoubleCentralizer NormedRing.toNorm instNormedRing 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 ContinuousLinearMap.hasOpNorm DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instRing Prod.instAddZeroClass ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toESeminormedAddMonoid AddMonoidHom.instFunLike toProdHom	—	—
norm_def' 📖	mathematical	—	Norm.norm DoubleCentralizer NormedRing.toNorm instNormedRing 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 MulOpposite Prod.toNorm ContinuousLinearMap.hasOpNorm MulOpposite.instNormedRing ContinuousLinearMap.toNormedRing DFunLike.coe RingHom Ring.toSemiring instRing Prod.instNonAssocSemiring ContinuousLinearMap.semiring IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing MulOpposite.instNonAssocSemiring RingHom.instFunLike toProdMulOppositeHom	—	—
norm_fst 📖	mathematical	—	Norm.norm 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 ContinuousLinearMap.hasOpNorm toProd DoubleCentralizer NormedRing.toNorm instNormedRing	—	norm_fst_eq_snd max_eq_right le_rfl
norm_fst_eq_snd 📖	mathematical	—	Norm.norm 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 ContinuousLinearMap.hasOpNorm toProd	—	RingHomIsometric.ids le_imp_le_of_le_of_le mul_le_mul_left covariant_swap_mul_of_covariant_mul NNReal.mulLeftMono mul_le_mul_right ContinuousLinearMap.le_opNNNorm le_refl Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.RingNF.mul_assoc_rev add_zero NNReal.div_le_of_le_mul ContinuousLinearMap.opNNNorm_le_bound NNReal.sqrt_sq NNReal.sqrt_mul NNReal.sqrt_le_sqrt LE.le.trans NNReal.rpow_two div_pow NNReal.sq_sqrt sq mul_self_div_self NNReal.rpow_le_rpow LT.lt.le two_pos Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid CStarRing.nnnorm_star_mul_self nnnorm_mul_le central nnnorm_star CStarRing.to_normedStarGroup CStarRing.nnnorm_self_mul_star mul_comm le_antisymm
norm_snd 📖	mathematical	—	Norm.norm 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 ContinuousLinearMap.hasOpNorm toProd DoubleCentralizer NormedRing.toNorm instNormedRing	—	norm_fst norm_fst_eq_snd
one_fst 📖	mathematical	—	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 toProd DoubleCentralizer instOne ContinuousLinearMap.one	—	—
one_snd 📖	mathematical	—	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 toProd DoubleCentralizer instOne ContinuousLinearMap.one	—	—
one_toProd 📖	mathematical	—	toProd DoubleCentralizer instOne 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.instOne ContinuousLinearMap.one	—	—
pow_fst 📖	mathematical	—	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 toProd DoubleCentralizer instPow Monoid.toNatPow MonoidWithZero.toMonoid ContinuousLinearMap.monoidWithZero	—	—
pow_snd 📖	mathematical	—	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 toProd DoubleCentralizer instPow Monoid.toNatPow MonoidWithZero.toMonoid ContinuousLinearMap.monoidWithZero	—	—
pow_toProd 📖	mathematical	—	toProd DoubleCentralizer instPow 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.instPow Monoid.toNatPow MonoidWithZero.toMonoid ContinuousLinearMap.monoidWithZero	—	—
range_toProd 📖	mathematical	—	Set.range 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 DoubleCentralizer toProd setOf	—	Set.ext central
range_toProdMulOpposite 📖	mathematical	—	Set.range 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 MulOpposite DoubleCentralizer toProdMulOpposite setOf	—	Set.ext central
smul_fst 📖	mathematical	—	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 toProd DoubleCentralizer instSMul ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul AddCommMonoid.toAddMonoid	—	—
smul_snd 📖	mathematical	—	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 toProd DoubleCentralizer instSMul ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul AddCommMonoid.toAddMonoid	—	—
smul_toProd 📖	mathematical	—	toProd DoubleCentralizer instSMul 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.instSMul ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul AddCommMonoid.toAddMonoid	—	—
star_fst 📖	mathematical	—	DFunLike.coe 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 ContinuousLinearMap.funLike toProd Star.star DoubleCentralizer instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing StarRing.toStarAddMonoid	—	—
star_snd 📖	mathematical	—	DFunLike.coe 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 ContinuousLinearMap.funLike toProd Star.star DoubleCentralizer instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing StarRing.toStarAddMonoid	—	—
sub_fst 📖	mathematical	—	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 toProd DoubleCentralizer instSub ContinuousLinearMap.sub NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup	—	—
sub_snd 📖	mathematical	—	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 toProd DoubleCentralizer instSub ContinuousLinearMap.sub NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup	—	—
sub_toProd 📖	mathematical	—	toProd DoubleCentralizer instSub 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.instSub ContinuousLinearMap.sub NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup	—	—
toProdHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom DoubleCentralizer 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 AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instRing Prod.instAddZeroClass ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toESeminormedAddMonoid AddMonoidHom.instFunLike toProdHom toProd	—	RingHomIsometric.ids
toProdMulOppositeHom_apply 📖	mathematical	—	DFunLike.coe RingHom DoubleCentralizer 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 MulOpposite Ring.toSemiring instRing Prod.instNonAssocSemiring ContinuousLinearMap.semiring IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing MulOpposite.instNonAssocSemiring RingHom.instFunLike toProdMulOppositeHom toProdMulOpposite	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing
toProdMulOpposite_injective 📖	mathematical	—	DoubleCentralizer 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 MulOpposite toProdMulOpposite	—	ext MulOpposite.op_injective
zero_fst 📖	mathematical	—	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 toProd DoubleCentralizer instZero ContinuousLinearMap.zero	—	—
zero_snd 📖	mathematical	—	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 toProd DoubleCentralizer instZero ContinuousLinearMap.zero	—	—
zero_toProd 📖	mathematical	—	toProd DoubleCentralizer instZero 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.instZero ContinuousLinearMap.zero	—	—

MultiplierAlgebra

Definitions

Name	Category	Theorems
«term𝓜(_,_)» 📖» "API Documentation")	CompOp	—

(root)

Definitions

Name	Category	Theorems
DoubleCentralizer 📖	CompData	56 math math: DoubleCentralizer.star_snd, DoubleCentralizer.intCast_snd, DoubleCentralizer.range_toProdMulOpposite, DoubleCentralizer.natCast_fst, DoubleCentralizer.nnnorm_def', DoubleCentralizer.zero_snd, DoubleCentralizer.pow_snd, DoubleCentralizer.nnnorm_snd, DoubleCentralizer.instIsScalarTower, DoubleCentralizer.smul_toProd, DoubleCentralizer.toProdMulOpposite_injective, DoubleCentralizer.norm_def', DoubleCentralizer.norm_def, DoubleCentralizer.nnnorm_def, DoubleCentralizer.neg_snd, DoubleCentralizer.range_toProd, DoubleCentralizer.add_fst, DoubleCentralizer.smul_fst, DoubleCentralizer.star_fst, DoubleCentralizer.add_snd, DoubleCentralizer.norm_snd, DoubleCentralizer.nnnorm_fst, DoubleCentralizer.neg_toProd, DoubleCentralizer.algebraMap_snd, DoubleCentralizer.one_snd, DoubleCentralizer.algebraMap_toProd, DoubleCentralizer.instIsCentralScalar, DoubleCentralizer.pow_toProd, DoubleCentralizer.zero_fst, DoubleCentralizer.instCStarRing, DoubleCentralizer.sub_toProd, DoubleCentralizer.one_fst, DoubleCentralizer.coeHom_apply, DoubleCentralizer.sub_fst, DoubleCentralizer.pow_fst, DoubleCentralizer.algebraMap_fst, DoubleCentralizer.mul_fst, DoubleCentralizer.coe_eq_algebraMap, DoubleCentralizer.zero_toProd, DoubleCentralizer.norm_fst, DoubleCentralizer.natCast_toProd, DoubleCentralizer.one_toProd, DoubleCentralizer.natCast_snd, DoubleCentralizer.sub_snd, DoubleCentralizer.instStarModule, DoubleCentralizer.intCast_fst, DoubleCentralizer.isUniformEmbedding_toProdMulOpposite, DoubleCentralizer.instCompleteSpace, DoubleCentralizer.toProdHom_apply, DoubleCentralizer.mul_snd, DoubleCentralizer.intCast_toProd, DoubleCentralizer.instSMulCommClass, DoubleCentralizer.smul_snd, DoubleCentralizer.add_toProd, DoubleCentralizer.neg_fst, DoubleCentralizer.toProdMulOppositeHom_apply

---

← Back to Index