Matrix

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

Statistics

Metric	Count
Definitions instL2OpMetricSpace, instL2OpNormedAddCommGroup, instL2OpNormedAlgebra, instL2OpNormedRing, instL2OpNormedSpace, l2OpNormedAddCommGroupAux, l2OpNormedRingAux, toEuclideanCLM	8
Theorems coe_toEuclideanCLM_eq_toEuclideanLin, cstar_nnnorm_def, cstar_norm_def, instCStarRing, l2_opNNNorm_conjTranspose, l2_opNNNorm_conjTranspose_mul_self, l2_opNNNorm_def, l2_opNNNorm_diagonal, l2_opNNNorm_mul, l2_opNNNorm_mulVec, l2_opNorm_conjTranspose, l2_opNorm_conjTranspose_mul_self, l2_opNorm_def, l2_opNorm_diagonal, l2_opNorm_mul, l2_opNorm_mulVec, l2_opNorm_toEuclideanCLM, ofLp_toEuclideanCLM, toEuclideanCLM_toLp, entry_norm_bound_of_unitary, entrywise_sup_norm_bound_of_unitary	21
Total	29

Matrix

Definitions

Name	Category	Theorems
instL2OpMetricSpace 📖	CompOp	—
instL2OpNormedAddCommGroup 📖	CompOp	13 math math: l2_opNorm_toEuclideanCLM, l2_opNorm_mulVec, l2_opNNNorm_mulVec, l2_opNorm_diagonal, l2_opNorm_conjTranspose_mul_self, l2_opNNNorm_conjTranspose, l2_opNorm_conjTranspose, l2_opNNNorm_mul, l2_opNNNorm_def, l2_opNNNorm_diagonal, l2_opNNNorm_conjTranspose_mul_self, l2_opNorm_def, l2_opNorm_mul
instL2OpNormedAlgebra 📖	CompOp	—
instL2OpNormedRing 📖	CompOp	6 math math: cstar_nnnorm_def, permMatrix_l2_opNorm_le, l2_opNorm_le_one_of_mem_doublyStochastic, instCStarRing, cstar_norm_def, permMatrix_l2_opNorm_eq
instL2OpNormedSpace 📖	CompOp	—
l2OpNormedAddCommGroupAux 📖	CompOp	—
l2OpNormedRingAux 📖	CompOp	—
toEuclideanCLM 📖	CompOp	6 math math: l2_opNorm_toEuclideanCLM, cstar_nnnorm_def, toEuclideanCLM_toLp, ofLp_toEuclideanCLM, coe_toEuclideanCLM_eq_toEuclideanLin, cstar_norm_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_toEuclideanCLM_eq_toEuclideanLin 📖	mathematical	—	ContinuousLinearMap.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring EuclideanSpace PiLp.topologicalSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid PiLp.normedAddCommGroup fact_one_le_two_ennreal NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing WithLp.instModule Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace DFunLike.coe StarAlgEquiv Matrix ContinuousLinearMap add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing ContinuousLinearMap.add IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup PiLp.seminormedAddCommGroup instMulOfFintypeOfAddCommMonoid Distrib.toMul ContinuousLinearMap.instMul smul Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid WithLp.instDistribMulAction Pi.distribMulAction SubNegMonoid.toAddMonoid Module.toDistribMulAction WithLp.instSMulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGroup.toAddCommMonoid Function.smulCommClass NormedAddCommGroup.toSeminormedAddCommGroup Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul PiLp.uniformSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsBoundedSMul.toUniformContinuousConstSMul PiLp.instPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid WithLp.instAddCommGroup NormedAddCommGroup.toAddCommGroup PiLp.instIsBoundedSMul NormedSpace.toIsBoundedSMul instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid RCLike.toStarRing ContinuousLinearMap.instStarId PiLp.innerProductSpace PiLp.completeSpace PseudoEMetricSpace.toUniformSpace PseudoMetricSpace.toPseudoEMetricSpace RCLike.toCompleteSpace StarAlgEquiv.instFunLike toEuclideanCLM LinearEquiv RingHomInvPair.ids LinearMap addCommMonoid LinearMap.addCommMonoid module LinearMap.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toEuclideanLin	—	fact_one_le_two_ennreal IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup WithLp.instSMulCommClass Function.smulCommClass Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul PiLp.instIsBoundedSMul NormedSpace.toIsBoundedSMul PiLp.completeSpace RCLike.toCompleteSpace
cstar_nnnorm_def 📖	mathematical	—	NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing instL2OpNormedRing ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring EuclideanSpace PiLp.topologicalSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid PiLp.normedAddCommGroup fact_one_le_two_ennreal NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing WithLp.instModule Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedSpace.toModule NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace ContinuousLinearMap.toSeminormedAddCommGroup PiLp.seminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField PiLp.normedSpace NontriviallyNormedField.toNormedField RingHomIsometric.ids DFunLike.coe StarAlgEquiv add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing ContinuousLinearMap.add IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup instMulOfFintypeOfAddCommMonoid Distrib.toMul ContinuousLinearMap.instMul smul Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid WithLp.instDistribMulAction Pi.distribMulAction SubNegMonoid.toAddMonoid Module.toDistribMulAction WithLp.instSMulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGroup.toAddCommMonoid Function.smulCommClass NormedAddCommGroup.toSeminormedAddCommGroup Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul PiLp.uniformSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsBoundedSMul.toUniformContinuousConstSMul PiLp.instPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid WithLp.instAddCommGroup NormedAddCommGroup.toAddCommGroup PiLp.instIsBoundedSMul NormedSpace.toIsBoundedSMul instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid RCLike.toStarRing ContinuousLinearMap.instStarId PiLp.innerProductSpace PiLp.completeSpace PseudoEMetricSpace.toUniformSpace PseudoMetricSpace.toPseudoEMetricSpace RCLike.toCompleteSpace StarAlgEquiv.instFunLike toEuclideanCLM	—	—
cstar_norm_def 📖	mathematical	—	Norm.norm Matrix NormedRing.toNorm instL2OpNormedRing ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring EuclideanSpace PiLp.topologicalSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid PiLp.normedAddCommGroup fact_one_le_two_ennreal NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing WithLp.instModule Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace ContinuousLinearMap.hasOpNorm PiLp.seminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField PiLp.normedSpace NontriviallyNormedField.toNormedField DFunLike.coe StarAlgEquiv add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing ContinuousLinearMap.add IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup instMulOfFintypeOfAddCommMonoid Distrib.toMul ContinuousLinearMap.instMul smul Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid WithLp.instDistribMulAction Pi.distribMulAction SubNegMonoid.toAddMonoid Module.toDistribMulAction WithLp.instSMulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGroup.toAddCommMonoid Function.smulCommClass NormedAddCommGroup.toSeminormedAddCommGroup Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul PiLp.uniformSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsBoundedSMul.toUniformContinuousConstSMul PiLp.instPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid WithLp.instAddCommGroup NormedAddCommGroup.toAddCommGroup PiLp.instIsBoundedSMul NormedSpace.toIsBoundedSMul instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid RCLike.toStarRing ContinuousLinearMap.instStarId PiLp.innerProductSpace PiLp.completeSpace PseudoEMetricSpace.toUniformSpace PseudoMetricSpace.toPseudoEMetricSpace RCLike.toCompleteSpace StarAlgEquiv.instFunLike toEuclideanCLM	—	—
instCStarRing 📖	mathematical	—	CStarRing Matrix NormedRing.toNonUnitalNormedRing instL2OpNormedRing instStarRing NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.toStarRing	—	le_of_eq l2_opNorm_conjTranspose_mul_self
l2_opNNNorm_conjTranspose 📖	mathematical	—	NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup instL2OpNormedAddCommGroup conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	—	l2_opNorm_conjTranspose
l2_opNNNorm_conjTranspose_mul_self 📖	mathematical	—	NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup instL2OpNormedAddCommGroup instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid RCLike.toStarRing NNReal NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	l2_opNorm_conjTranspose_mul_self
l2_opNNNorm_def 📖	mathematical	—	NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup instL2OpNormedAddCommGroup ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring EuclideanSpace PiLp.topologicalSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField AddCommGroup.toAddCommMonoid WithLp.instAddCommGroup Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing WithLp.instModule Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace ContinuousLinearMap.toSeminormedAddCommGroup PiLp.seminormedAddCommGroup fact_one_le_two_ennreal PiLp.normedSpace RingHomIsometric.ids DFunLike.coe LinearEquiv RingHomInvPair.ids addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup module ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction CommRing.toRing ContinuousSMul.continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.continuousSMul PiLp.instPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid PiLp.instIsBoundedSMul NormedSpace.toIsBoundedSMul EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.trans LinearMap PiLp.normedAddCommGroup LinearMap.addCommMonoid LinearMap.module WithLp.instSMulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Function.smulCommClass Algebra.to_smulCommClass Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id RingHomCompTriple.ids toEuclideanLin LinearMap.toContinuousLinearMap RCLike.toCompleteSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace PiLp.instEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace WithLp.instModuleFinite DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing FiniteDimensional.finiteDimensional_pi' Finite.of_fintype Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self	—	—
l2_opNNNorm_diagonal 📖	mathematical	—	NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup instL2OpNormedAddCommGroup diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Pi.seminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing	—	l2_opNorm_diagonal
l2_opNNNorm_mul 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm Matrix SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup instL2OpNormedAddCommGroup instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	l2_opNorm_mul
l2_opNNNorm_mulVec 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm EuclideanSpace SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup PiLp.seminormedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing PiLp.topologicalSpace AddCommGroup.toAddCommMonoid WithLp.instAddCommGroup Pi.addCommGroup NormedAddCommGroup.toAddCommGroup Pi.Function.module NormedSpace.toModule InnerProductSpace.toNormedSpace RCLike.innerProductSpace WithLp.instModule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm EuclideanSpace.equiv mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing WithLp.ofLp Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring instSemiringNNReal Matrix NormedAddCommGroup.toSeminormedAddCommGroup instL2OpNormedAddCommGroup	—	l2_opNorm_mulVec
l2_opNorm_conjTranspose 📖	mathematical	—	Norm.norm Matrix NormedAddCommGroup.toNorm instL2OpNormedAddCommGroup conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	—	fact_one_le_two_ennreal RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self ContinuousSMul.continuousConstSMul IsBoundedSMul.continuousSMul PiLp.instIsBoundedSMul NormedSpace.toIsBoundedSMul WithLp.instSMulCommClass Function.smulCommClass Algebra.to_smulCommClass RingHomCompTriple.ids RCLike.toCompleteSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self l2_opNorm_def toEuclideanLin_eq_toLin_orthonormal LinearEquiv.trans_apply RingHomInvPair.instStarRingEnd toLin_conjTranspose RingHomIsometric.ids UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul FiniteDimensional.complete SeminormedAddCommGroup.to_isUniformAddGroup LinearMap.adjoint_toContinuousLinearMap LinearIsometryEquiv.norm_map
l2_opNorm_conjTranspose_mul_self 📖	mathematical	—	Norm.norm Matrix NormedAddCommGroup.toNorm instL2OpNormedAddCommGroup instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid RCLike.toStarRing Real Real.instMul	—	fact_one_le_two_ennreal RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self ContinuousSMul.continuousConstSMul IsBoundedSMul.continuousSMul PiLp.instIsBoundedSMul NormedSpace.toIsBoundedSMul WithLp.instSMulCommClass Function.smulCommClass Algebra.to_smulCommClass RingHomCompTriple.ids RCLike.toCompleteSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self l2_opNorm_def toEuclideanLin_eq_toLin_orthonormal LinearEquiv.trans_apply toLin_mul RingHomInvPair.instStarRingEnd toLin_conjTranspose ContinuousLinearMap.norm_adjoint_comp_self PiLp.completeSpace
l2_opNorm_def 📖	mathematical	—	Norm.norm Matrix NormedAddCommGroup.toNorm instL2OpNormedAddCommGroup ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring EuclideanSpace PiLp.topologicalSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField AddCommGroup.toAddCommMonoid WithLp.instAddCommGroup Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing WithLp.instModule Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace ContinuousLinearMap.hasOpNorm PiLp.seminormedAddCommGroup fact_one_le_two_ennreal PiLp.normedSpace DFunLike.coe LinearEquiv RingHomInvPair.ids addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup module ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction CommRing.toRing ContinuousSMul.continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.continuousSMul PiLp.instPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid PiLp.instIsBoundedSMul NormedSpace.toIsBoundedSMul EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.trans LinearMap PiLp.normedAddCommGroup LinearMap.addCommMonoid LinearMap.module WithLp.instSMulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Function.smulCommClass Algebra.to_smulCommClass Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id RingHomCompTriple.ids toEuclideanLin LinearMap.toContinuousLinearMap RCLike.toCompleteSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace PiLp.instEMetricSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace WithLp.instModuleFinite DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing FiniteDimensional.finiteDimensional_pi' Finite.of_fintype Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self	—	—
l2_opNorm_diagonal 📖	mathematical	—	Norm.norm Matrix NormedAddCommGroup.toNorm instL2OpNormedAddCommGroup diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedRing.toNorm Pi.normedRing NormedCommRing.toNormedRing	—	fact_one_le_two_ennreal IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup WithLp.instSMulCommClass Function.smulCommClass Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul PiLp.instIsBoundedSMul NormedSpace.toIsBoundedSMul PiLp.completeSpace RCLike.toCompleteSpace l2_opNorm_toEuclideanCLM le_antisymm ContinuousLinearMap.opNorm_le_bound norm_nonneg sq_le_sq₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing mul_nonneg IsOrderedRing.toPosMulMono EuclideanSpace.norm_sq_eq Finset.sum_congr mulVec_diagonal norm_mul NormedDivisionRing.toNormMulClass Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_pow le_imp_le_of_le_of_le mul_le_mul_of_nonneg_right pow_le_pow_left₀ norm_le_pi_norm Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE Nat.instAtLeastTwoHAddOfNat even_two_mul le_refl Finset.mul_sum RingHomIsometric.ids pi_norm_le_iff_of_nonneg toEuclideanCLM_toLp mulVec_single col_diagonal one_smul EuclideanSpace.norm_single ContinuousLinearMap.le_opNorm CStarRing.norm_of_mem_unitary RCLike.instCStarRing IsLocalRing.toNontrivial Field.instIsLocalRing SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass mul_one
l2_opNorm_mul 📖	mathematical	—	Real Real.instLE Norm.norm Matrix NormedAddCommGroup.toNorm instL2OpNormedAddCommGroup instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing Real.instMul	—	fact_one_le_two_ennreal RingHomCompTriple.ids RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self ContinuousSMul.continuousConstSMul IsBoundedSMul.continuousSMul PiLp.instIsBoundedSMul NormedSpace.toIsBoundedSMul WithLp.instSMulCommClass Function.smulCommClass Algebra.to_smulCommClass RCLike.toCompleteSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self ContinuousLinearMap.opNorm_comp_le RingHomIsometric.ids ContinuousLinearMap.ext Nat.instAtLeastTwoHAddOfNat toLin'_mul
l2_opNorm_mulVec 📖	mathematical	—	Real Real.instLE Norm.norm EuclideanSpace PiLp.instNorm ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal NormedField.toNorm DenselyNormedField.toNormedField RCLike.toDenselyNormedField DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing PiLp.topologicalSpace AddCommGroup.toAddCommMonoid WithLp.instAddCommGroup Pi.addCommGroup NormedAddCommGroup.toAddCommGroup Pi.Function.module NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace WithLp.instModule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm EuclideanSpace.equiv mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing WithLp.ofLp Real.instMul Matrix NormedAddCommGroup.toNorm instL2OpNormedAddCommGroup	—	ContinuousLinearMap.le_opNorm fact_one_le_two_ennreal RingHomIsometric.ids RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self ContinuousSMul.continuousConstSMul IsBoundedSMul.continuousSMul PiLp.instIsBoundedSMul NormedSpace.toIsBoundedSMul WithLp.instSMulCommClass Function.smulCommClass Algebra.to_smulCommClass RingHomCompTriple.ids RCLike.toCompleteSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self
l2_opNorm_toEuclideanCLM 📖	mathematical	—	Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring EuclideanSpace PiLp.topologicalSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid PiLp.normedAddCommGroup fact_one_le_two_ennreal NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing WithLp.instModule Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace ContinuousLinearMap.hasOpNorm PiLp.seminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField PiLp.normedSpace NontriviallyNormedField.toNormedField DFunLike.coe StarAlgEquiv Matrix add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing ContinuousLinearMap.add IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup instMulOfFintypeOfAddCommMonoid Distrib.toMul ContinuousLinearMap.instMul smul Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid WithLp.instDistribMulAction Pi.distribMulAction SubNegMonoid.toAddMonoid Module.toDistribMulAction WithLp.instSMulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGroup.toAddCommMonoid Function.smulCommClass NormedAddCommGroup.toSeminormedAddCommGroup Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul PiLp.uniformSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsBoundedSMul.toUniformContinuousConstSMul PiLp.instPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid WithLp.instAddCommGroup NormedAddCommGroup.toAddCommGroup PiLp.instIsBoundedSMul NormedSpace.toIsBoundedSMul instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid RCLike.toStarRing ContinuousLinearMap.instStarId PiLp.innerProductSpace PiLp.completeSpace PseudoEMetricSpace.toUniformSpace PseudoMetricSpace.toPseudoEMetricSpace RCLike.toCompleteSpace StarAlgEquiv.instFunLike toEuclideanCLM NormedAddCommGroup.toNorm instL2OpNormedAddCommGroup	—	fact_one_le_two_ennreal IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup WithLp.instSMulCommClass Function.smulCommClass Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul PiLp.instIsBoundedSMul NormedSpace.toIsBoundedSMul PiLp.completeSpace RCLike.toCompleteSpace
ofLp_toEuclideanCLM 📖	mathematical	—	WithLp.ofLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring EuclideanSpace PiLp.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid PiLp.normedAddCommGroup fact_one_le_two_ennreal NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing WithLp.instModule Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace ContinuousLinearMap.funLike StarAlgEquiv Matrix add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing ContinuousLinearMap.add IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup PiLp.seminormedAddCommGroup instMulOfFintypeOfAddCommMonoid Distrib.toMul ContinuousLinearMap.instMul smul Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid WithLp.instDistribMulAction Pi.distribMulAction SubNegMonoid.toAddMonoid Module.toDistribMulAction WithLp.instSMulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGroup.toAddCommMonoid Function.smulCommClass NormedAddCommGroup.toSeminormedAddCommGroup Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul PiLp.uniformSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsBoundedSMul.toUniformContinuousConstSMul PiLp.instPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid WithLp.instAddCommGroup NormedAddCommGroup.toAddCommGroup PiLp.instIsBoundedSMul NormedSpace.toIsBoundedSMul instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid RCLike.toStarRing ContinuousLinearMap.instStarId PiLp.innerProductSpace PiLp.completeSpace PseudoEMetricSpace.toUniformSpace PseudoMetricSpace.toPseudoEMetricSpace RCLike.toCompleteSpace StarAlgEquiv.instFunLike toEuclideanCLM mulVec	—	fact_one_le_two_ennreal IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup WithLp.instSMulCommClass Function.smulCommClass Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul PiLp.instIsBoundedSMul NormedSpace.toIsBoundedSMul PiLp.completeSpace RCLike.toCompleteSpace
toEuclideanCLM_toLp 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring EuclideanSpace PiLp.topologicalSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid PiLp.normedAddCommGroup fact_one_le_two_ennreal NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing WithLp.instModule Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace ContinuousLinearMap.funLike StarAlgEquiv Matrix add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing ContinuousLinearMap.add IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup PiLp.seminormedAddCommGroup instMulOfFintypeOfAddCommMonoid Distrib.toMul ContinuousLinearMap.instMul smul Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid WithLp.instDistribMulAction Pi.distribMulAction SubNegMonoid.toAddMonoid Module.toDistribMulAction WithLp.instSMulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGroup.toAddCommMonoid Function.smulCommClass NormedAddCommGroup.toSeminormedAddCommGroup Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul PiLp.uniformSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsBoundedSMul.toUniformContinuousConstSMul PiLp.instPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid WithLp.instAddCommGroup NormedAddCommGroup.toAddCommGroup PiLp.instIsBoundedSMul NormedSpace.toIsBoundedSMul instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid RCLike.toStarRing ContinuousLinearMap.instStarId PiLp.innerProductSpace PiLp.completeSpace PseudoEMetricSpace.toUniformSpace PseudoMetricSpace.toPseudoEMetricSpace RCLike.toCompleteSpace StarAlgEquiv.instFunLike toEuclideanCLM WithLp.toLp mulVec	—	fact_one_le_two_ennreal IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup WithLp.instSMulCommClass Function.smulCommClass Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul PiLp.instIsBoundedSMul NormedSpace.toIsBoundedSMul PiLp.completeSpace RCLike.toCompleteSpace

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
entry_norm_bound_of_unitary 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField SetLike.instMembership Submonoid.instSetLike Matrix.unitaryGroup RCLike.toStarRing	Real Real.instLE Norm.norm NormedField.toNorm Real.instOne	—	Multiset.single_le_sum Real.instIsOrderedAddMonoid Multiset.mem_map sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono Finset.sum_congr RCLike.mul_conj Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing IsLocalRing.toNontrivial Field.instIsLocalRing RCLike.ext_iff RCLike.ofReal_re Unitary.mul_star_self_of_mem Matrix.one_apply_eq RCLike.one_re sq_le_one_iff₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass norm_nonneg
entrywise_sup_norm_bound_of_unitary 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField SetLike.instMembership Submonoid.instSetLike Matrix.unitaryGroup RCLike.toStarRing	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm Matrix.normedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing Real.instOne	—	pi_norm_le_iff_of_nonneg zero_le_one Real.instZeroLEOneClass entry_norm_bound_of_unitary

---

← Back to Index