Basic

📁 Source: Mathlib/Analysis/Normed/Module/Multilinear/Basic.lean

Statistics

Metric	Count
Definitions continuousMultilinearMapCongrLeft, continuousMultilinearMapCongrRight, compContinuousMultilinearMapL, flipMultilinear, flipMultilinearEquiv, flipMultilinearEquivₗ, compContinuousLinearMapContinuousMultilinear, compContinuousLinearMapL, compContinuousLinearMapLRight, compContinuousLinearMapMultilinear, fderivCompContinuousLinearMap, flipLinear, hasOpNorm, hasOpNorm', instPseudoMetricSpace, iteratedFDeriv, iteratedFDerivComponent, normedAddCommGroup, normedAddCommGroup', normedSpace, normedSpace', ofSubsingletonₗᵢ, opNorm, piFieldEquiv, piₗᵢ, prodL, restr, restrictScalarsₗᵢ, seminorm, seminormedAddCommGroup, seminormedAddCommGroup', smulRightL, mkContinuous, mkContinuousLinear, mkContinuousMultilinear	35
Theorems continuousMultilinearMapCongrLeft_apply, continuousMultilinearMapCongrLeft_symm, continuousMultilinearMapCongrRight_apply, continuousMultilinearMapCongrRight_symm, coe_flipMultilinearEquiv, coe_symm_flipMultilinearEquiv, continuousAt_uncurry_of_multilinear, continuousOn_uncurry_of_multilinear, continuousWithinAt_uncurry_of_multilinear, continuous_uncurry_of_multilinear, flipLinear_flipMultilinear, flipMultilinear_apply_apply, norm_compContinuousMultilinearMap_le, bounds_bddBelow, bounds_nonempty, compContinuousLinearMapContinuousMultilinear_apply_apply, compContinuousLinearMapLRight_apply, compContinuousLinearMapL_apply, fderivCompContinuousLinearMap_apply, flipLinear_apply_apply, flipMultilinear_flipLinear, instContinuousEval, instIsBoundedSMul, isLeast_opNNNorm, isLeast_opNorm, iteratedFDerivComponent_apply, le_mul_prod_of_opNorm_le_of_le, le_of_opNNNorm_le, le_of_opNorm_le, le_opNNNorm, le_opNorm, le_opNorm_mul_pow_card_of_le, le_opNorm_mul_pow_of_le, le_opNorm_mul_prod_of_le, nnnorm_constOfIsEmpty, nnnorm_ofSubsingleton, nnnorm_ofSubsingleton_id, nnnorm_ofSubsingleton_id_le, nnnorm_smulRight, norm_compContinuousLinearMapLRight_le, norm_compContinuousLinearMapL_le, norm_compContinuousLinearMap_le, norm_compContinuous_linearIsometryEquiv, norm_compContinuous_linearIsometry_le, norm_constOfIsEmpty, norm_def, norm_image_sub_le, norm_image_sub_le', norm_iteratedFDerivComponent_le, norm_iteratedFDeriv_le', norm_mkPiAlgebra, norm_mkPiAlgebraFin, norm_mkPiAlgebraFin_le, norm_mkPiAlgebraFin_le_of_pos, norm_mkPiAlgebraFin_succ_le, norm_mkPiAlgebraFin_zero, norm_mkPiAlgebra_le, norm_mkPiAlgebra_of_empty, norm_mkPiRing, norm_ofSubsingleton, norm_ofSubsingleton_id, norm_ofSubsingleton_id_le, norm_restr, norm_restrictScalars, norm_smulRight, norm_smulRightL_le, ofSubsingletonₗᵢ_apply, ofSubsingletonₗᵢ_symm_apply, opNNNorm_le_iff, opNNNorm_pi, opNNNorm_prod, opNorm_add_le, opNorm_le_bound, opNorm_le_iff, opNorm_nonneg, opNorm_pi, opNorm_prod, opNorm_smul_le, opNorm_zero, opNorm_zero_iff, piₗᵢ_apply, piₗᵢ_symm_apply, prodL_apply, prodL_symm_apply, ratio_le_opNorm, smulRightL_apply, unit_le_opNorm, norm_compContinuousMultilinearMap, bound_of_shell, bound_of_shell_of_continuous, bound_of_shell_of_norm_map_coord_zero, coe_mkContinuous, continuous_of_bound, exists_bound_of_continuous, mkContinuousLinear_norm_le, mkContinuousLinear_norm_le', mkContinuousMultilinear_apply, mkContinuousMultilinear_norm_le, mkContinuousMultilinear_norm_le', mkContinuous_norm_le, mkContinuous_norm_le', norm_image_sub_le_of_bound, norm_image_sub_le_of_bound', norm_map_coord_zero, restr_norm_le	105
Total	140

ContinuousLinearEquiv

Definitions

Name	Category	Theorems
continuousMultilinearMapCongrLeft 📖	CompOp	2 math math: continuousMultilinearMapCongrLeft_apply, continuousMultilinearMapCongrLeft_symm
continuousMultilinearMapCongrRight 📖	CompOp	2 math math: continuousMultilinearMapCongrRight_symm, continuousMultilinearMapCongrRight_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousMultilinearMapCongrLeft_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap.instTopologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup ContinuousMultilinearMap.instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction 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 smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing EquivLike.toFunLike equivLike continuousMultilinearMapCongrLeft ContinuousMultilinearMap.compContinuousLinearMap toContinuousLinearMap	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self
continuousMultilinearMapCongrLeft_symm 📖	mathematical	—	symm DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap.instTopologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup ContinuousMultilinearMap.instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction 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 smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing continuousMultilinearMapCongrLeft	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self
continuousMultilinearMapCongrRight_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap.instTopologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup ContinuousMultilinearMap.instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction 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 smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing EquivLike.toFunLike equivLike continuousMultilinearMapCongrRight ContinuousLinearMap.compContinuousMultilinearMap toContinuousLinearMap	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self
continuousMultilinearMapCongrRight_symm 📖	mathematical	—	symm DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap.instTopologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup ContinuousMultilinearMap.instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction 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 smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing continuousMultilinearMapCongrRight	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self

ContinuousLinearMap

Definitions

Name	Category	Theorems
compContinuousMultilinearMapL 📖	CompOp	—
flipMultilinear 📖	CompOp	12 math math: HasFDerivWithinAt.linear_multilinear_comp, HasFDerivAt.continuousMultilinear_apply_const, flipMultilinear_apply_apply, fderivWithin_continuousMultilinear_apply_const, coe_flipMultilinearEquiv, HasStrictFDerivAt.continuousMultilinear_apply_const, HasFDerivWithinAt.continuousMultilinear_apply_const, fderiv_continuousMultilinear_apply_const, hasFDerivAt_uncurry_of_multilinear, HasFDerivAt.linear_multilinear_comp, ContinuousMultilinearMap.flipMultilinear_flipLinear, flipLinear_flipMultilinear
flipMultilinearEquiv 📖	CompOp	2 math math: coe_flipMultilinearEquiv, coe_symm_flipMultilinearEquiv
flipMultilinearEquivₗ 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_flipMultilinearEquiv 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousLinearMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup ContinuousMultilinearMap NormedSpace.toModule ContinuousMultilinearMap.instTopologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup ContinuousMultilinearMap.instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction 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 smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing topologicalSpace ContinuousMultilinearMap.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing ContinuousMultilinearMap.instIsTopologicalAddGroup addCommMonoid ContinuousMultilinearMap.seminormedAddCommGroup module addCommGroup topologicalAddGroup toSeminormedAddCommGroup RingHomIsometric.ids ContinuousMultilinearMap.instSMulCommClass ContinuousMultilinearMap.instContinuousConstSMul continuousConstSMul smulCommClass EquivLike.toFunLike ContinuousLinearEquiv.equivLike flipMultilinearEquiv flipMultilinear	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self RingHomInvPair.ids ContinuousMultilinearMap.instIsTopologicalAddGroup topologicalAddGroup RingHomIsometric.ids ContinuousMultilinearMap.instSMulCommClass ContinuousMultilinearMap.instContinuousConstSMul continuousConstSMul smulCommClass
coe_symm_flipMultilinearEquiv 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap ContinuousLinearMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup 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 topologicalSpace ContinuousMultilinearMap.instTopologicalSpace addCommGroup NormedRing.toRing NormedCommRing.toNormedRing topologicalAddGroup ContinuousMultilinearMap.addCommMonoid toSeminormedAddCommGroup RingHomIsometric.ids ContinuousMultilinearMap.instModule ContinuousMultilinearMap.instAddCommGroup ContinuousMultilinearMap.instIsTopologicalAddGroup ContinuousMultilinearMap.seminormedAddCommGroup continuousConstSMul smulCommClass ContinuousMultilinearMap.instSMulCommClass ContinuousMultilinearMap.instContinuousConstSMul EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm flipMultilinearEquiv ContinuousMultilinearMap.flipLinear	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomInvPair.ids topologicalAddGroup RingHomIsometric.ids ContinuousMultilinearMap.instIsTopologicalAddGroup continuousConstSMul smulCommClass ContinuousMultilinearMap.instSMulCommClass ContinuousMultilinearMap.instContinuousConstSMul
continuousAt_uncurry_of_multilinear 📖	mathematical	—	ContinuousAt instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousMultilinearMap.funLike ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousMultilinearMap.instTopologicalSpace ContinuousMultilinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousMultilinearMap.instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing funLike	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self Continuous.continuousAt continuous_uncurry_of_multilinear
continuousOn_uncurry_of_multilinear 📖	mathematical	—	ContinuousOn instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousMultilinearMap.funLike ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousMultilinearMap.instTopologicalSpace ContinuousMultilinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousMultilinearMap.instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing funLike	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self Continuous.continuousOn continuous_uncurry_of_multilinear
continuousWithinAt_uncurry_of_multilinear 📖	mathematical	—	ContinuousWithinAt instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousMultilinearMap.funLike ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousMultilinearMap.instTopologicalSpace ContinuousMultilinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousMultilinearMap.instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing funLike	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self Continuous.continuousWithinAt continuous_uncurry_of_multilinear
continuous_uncurry_of_multilinear 📖	mathematical	—	Continuous instTopologicalSpaceProd Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousMultilinearMap.funLike ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousMultilinearMap.instTopologicalSpace ContinuousMultilinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousMultilinearMap.instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing funLike	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self Continuous.eval ContinuousMultilinearMap.instContinuousEval Continuous.comp' continuous Continuous.fst continuous_id' Continuous.snd
flipLinear_flipMultilinear 📖	mathematical	—	ContinuousMultilinearMap.flipLinear flipMultilinear	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self
flipMultilinear_apply_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule funLike ContinuousMultilinearMap addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction 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 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 topologicalSpace ContinuousMultilinearMap.funLike flipMultilinear ContinuousMultilinearMap.instTopologicalSpace ContinuousMultilinearMap.addCommMonoid ContinuousMultilinearMap.instModule	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self
norm_compContinuousMultilinearMap_le 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap.hasOpNorm compContinuousMultilinearMap Real.instMul ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring hasOpNorm	—	ContinuousMultilinearMap.opNorm_le_bound mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing norm_nonneg RingHomIsometric.ids le_opNorm_of_le ContinuousMultilinearMap.le_opNorm mul_assoc

ContinuousMultilinearMap

Definitions

Name	Category	Theorems
compContinuousLinearMapContinuousMultilinear 📖	CompOp	1 math math: compContinuousLinearMapContinuousMultilinear_apply_apply
compContinuousLinearMapL 📖	CompOp	8 math math: HasFDerivWithinAt.continuousMultilinearMapCompContinuousLinearMap, HasFDerivAt.continuousMultilinearMapCompContinuousLinearMap, fderivWithin_continuousMultilinearMapCompContinuousLinearMap, fderiv_continuousMultilinearMapCompContinuousLinearMap, hasStrictFDerivAt_compContinuousLinearMap, HasStrictFDerivAt.continuousMultilinearMapCompContinuousLinearMap, compContinuousLinearMapL_apply, norm_compContinuousLinearMapL_le
compContinuousLinearMapLRight 📖	CompOp	3 math math: norm_compContinuousLinearMapLRight_le, VectorFourier.fourierPowSMulRight_eq_comp, compContinuousLinearMapLRight_apply
compContinuousLinearMapMultilinear 📖	CompOp	—
fderivCompContinuousLinearMap 📖	CompOp	8 math math: HasFDerivWithinAt.continuousMultilinearMapCompContinuousLinearMap, HasFDerivAt.continuousMultilinearMapCompContinuousLinearMap, fderivWithin_continuousMultilinearMapCompContinuousLinearMap, ContinuousAlternatingMap.toContinuousMultilinearMapCLM_comp_fderivCompContinuousLinearMap, fderiv_continuousMultilinearMapCompContinuousLinearMap, hasStrictFDerivAt_compContinuousLinearMap, HasStrictFDerivAt.continuousMultilinearMapCompContinuousLinearMap, fderivCompContinuousLinearMap_apply
flipLinear 📖	CompOp	4 math math: flipLinear_apply_apply, flipMultilinear_flipLinear, ContinuousLinearMap.coe_symm_flipMultilinearEquiv, ContinuousLinearMap.flipLinear_flipMultilinear
hasOpNorm 📖	CompOp	50 math math: norm_iteratedFDerivComponent_le, norm_map_snoc_le, ContinuousLinearMap.norm_compContinuousMultilinearMap_le, norm_compContinuousLinearMapLRight_le, opNorm_zero_iff, OrderedFinpartition.norm_compAlongOrderedFinpartitionL_apply_le, unit_le_opNorm, curryRight_norm, norm_compContinuous_linearIsometry_le, opNorm_smul_le, norm_image_sub_le, curryLeft_norm, le_opNorm, LinearIsometry.norm_compContinuousMultilinearMap, isLeast_opNorm, opNorm_nonneg, PiTensorProduct.norm_eval_le_injectiveSeminorm, norm_map_init_le, opNorm_zero, PiTensorProduct.liftEquiv_apply, opNorm_pi, opNorm_add_le, norm_restrictScalars, ratio_le_opNorm, ContinuousLinearMap.norm_uncurryMid, ContinuousLinearMap.uncurryLeft_norm, MultilinearMap.mkContinuousMultilinear_norm_le', norm_iteratedFDeriv_le, norm_iteratedFDeriv_le', le_opNorm_mul_pow_card_of_le, MultilinearMap.mkContinuous_norm_le, MultilinearMap.mkContinuousMultilinear_norm_le, le_opNorm_mul_prod_of_le, PiTensorProduct.norm_eval_le_projectiveSeminorm, norm_compContinuous_linearIsometryEquiv, norm_map_insertNth_le, opNorm_le_iff, norm_map_cons_le, norm_smulRight, opNorm_le_bound, norm_def, norm_constOfIsEmpty, le_opNorm_mul_pow_of_le, opNorm_prod, norm_compContinuousLinearMap_le, MultilinearMap.mkContinuous_norm_le', PiTensorProduct.mapLMultilinear_opNorm, norm_image_sub_le', norm_curryMid, uncurryRight_norm
hasOpNorm' 📖	CompOp	99 math math: norm_mkPiRing, ModularFormClass.qExpansionFormalMultilinearSeries_apply_norm, norm_iteratedFDerivComponent_le, ContDiffMapSupportedIn.norm_iteratedFDeriv_apply_le_seminorm, norm_iteratedFDerivWithin_smul_le, norm_iteratedFDerivWithin_one, norm_iteratedFDeriv_mul_le, norm_iteratedFDerivWithin_clm_apply, FormalMultilinearSeries.norm_le_div_pow_of_pos_of_lt_radius, ContDiffPointwiseHolderAt.isBigO, SchwartzMap.decay', OrderedFinpartition.norm_compAlongOrderedFinpartition_le, OrderedFinpartition.norm_applyOrderedFinpartition_le, ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear_of_le_one, norm_iteratedFDeriv_clm_apply, OrderedFinpartition.norm_compAlongOrderedFinpartitionL_apply_le, norm_mkPiAlgebra_le, formalMultilinearSeries_geometric_apply_norm_le, Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform_aux, norm_iteratedFDerivWithin_zero, ContinuousLinearMap.norm_iteratedFDerivWithin_comp_left, norm_iteratedFDerivWithin_clm_apply_const, FormalMultilinearSeries.norm_apply_eq_norm_coef, ContDiffMapSupportedIn.seminorm_le_iff, norm_restr, Function.hasTemperateGrowth_iff_isBigO, uncurry0_norm, norm_cauchyPowerSeries_le, norm_mkPiAlgebraFin_zero, SchwartzMap.norm_iteratedFDeriv_le_seminorm, FormalMultilinearSeries.compAlongComposition_bound, FormalMultilinearSeries.ofScalars_norm_le, norm_mkPiAlgebraFin_le_of_pos, ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear, contDiffPointwiseHolderAt_iff, LinearIsometry.norm_iteratedFDeriv_comp_left, norm_iteratedFDerivWithin_prod_le, FormalMultilinearSeries.not_summable_norm_of_radius_lt_nnnorm, FormalMultilinearSeries.norm_compContinuousLinearMap_le, Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform, LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left, ContinuousAlternatingMap.norm_toContinuousMultilinearMap, FormalMultilinearSeries.isLittleO_one_of_lt_radius, FormalMultilinearSeries.le_mul_pow_of_radius_pos, norm_mkPiAlgebra, norm_fderiv_iteratedFDeriv, ContDiffMapSupportedIn.seminorm_le_iff_withOrder, SchwartzMap.integral_pow_mul_iteratedFDeriv_le, LinearIsometry.norm_iteratedFDerivWithin_comp_left, norm_fderivWithin_iteratedFDerivWithin, ContinuousLinearMap.norm_iteratedFDeriv_comp_left, FormalMultilinearSeries.compAlongComposition_norm, formalMultilinearSeries_geometric_apply_norm, SchwartzMap.le_seminorm, norm_ofSubsingleton_id_le, FormalMultilinearSeries.norm_mul_pow_le_mul_pow_of_lt_radius, LinearIsometryEquiv.norm_iteratedFDeriv_comp_right, norm_iteratedFDeriv_le, norm_iteratedFDeriv_le', ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear, ContDiffMapSupportedIn.norm_iteratedFDeriv_apply_le_seminorm_withOrder, FormalMultilinearSeries.isLittleO_of_lt_radius, norm_mkPiAlgebraFin_le, LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_right, norm_iteratedFDeriv_prod_le, norm_domDomCongr, curry0_norm, norm_iteratedFDeriv_one, norm_mkPiAlgebraFin_succ_le, SchwartzMap.decay, OrderedFinpartition.norm_compAlongOrderedFinpartition_sub_compAlongOrderedFinpartition_le, ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one, norm_mkPiAlgebra_of_empty, ContDiffMapSupportedIn.bounded_iteratedFDeriv, norm_ofSubsingleton, VectorFourier.norm_fourierPowSMulRight_le, norm_iteratedFDerivWithin_mul_le, FormalMultilinearSeries.radius_eq_top_iff_summable_norm, FormalMultilinearSeries.summable_norm_mul_pow, norm_iteratedFDerivWithin_fderivWithin, norm_iteratedFDeriv_smul_le, FormalMultilinearSeries.norm_changeOriginSeriesTerm, norm_iteratedFDeriv_zero, norm_iteratedFDeriv_eq_norm_iteratedDeriv, norm_iteratedFDerivWithin_eq_norm_iteratedDerivWithin, LinearIsometryEquiv.norm_iteratedFDeriv_comp_left, SchwartzMap.one_add_le_sup_seminorm_apply, SchwartzMap.integrable_pow_mul_iteratedFDeriv, Function.HasTemperateGrowth.isBigO_uniform, FormalMultilinearSeries.norm_mul_pow_le_of_lt_radius, FormalMultilinearSeries.ofScalars_norm_eq_mul, fin0_apply_norm, norm_mkPiAlgebraFin, norm_iteratedFDeriv_fderiv, Function.HasTemperateGrowth.isBigO, FormalMultilinearSeries.ofScalars_norm, norm_ofSubsingleton_id, ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_aux, norm_iteratedFDeriv_clm_apply_const
instPseudoMetricSpace 📖	CompOp	18 math math: ContDiffMapSupportedIn.structureMapCLM_eq_of_scalars, ContDiffMapSupportedIn.structureMapCLM_apply, dist_iteratedFDerivWithin_one, ContDiffMapSupportedIn.structureMapLM_eq_of_scalars, ContDiffMapSupportedIn.uniformSpace_eq_iInf, ContDiffMapSupportedIn.continuous_iff_comp_withOrder, ContDiffMapSupportedIn.structureMapCLM_zero_apply, ContDiffMapSupportedIn.structureMapLM_apply_withOrder, dist_iteratedFDerivWithin_zero, instIsBoundedSMul, ContDiffMapSupportedIn.isUniformEmbedding_pi_structureMapCLM, ContDiffMapSupportedIn.structureMapCLM_apply_withOrder, ContDiffMapSupportedIn.seminorm_apply, ContDiffMapSupportedIn.structureMapLM_zero_injective, ContDiffMapSupportedIn.continuous_iff_comp, ContDiffMapSupportedIn.structureMapCLM_zero_injective, ContDiffMapSupportedIn.structureMapLM_zero_apply, ContDiffMapSupportedIn.structureMapLM_apply
iteratedFDeriv 📖	CompOp	3 math math: hasFTaylorSeriesUpTo_iteratedFDeriv, iteratedFDeriv_eq, norm_iteratedFDeriv_le'
iteratedFDerivComponent 📖	CompOp	2 math math: norm_iteratedFDerivComponent_le, iteratedFDerivComponent_apply
normedAddCommGroup 📖	CompOp	17 math math: analyticAt_uncurry_compContinuousLinearMap, HasFDerivWithinAt.continuousMultilinearMapCompContinuousLinearMap, HasFDerivAt.continuousMultilinearMapCompContinuousLinearMap, Real.fourierIntegral_continuousMultilinearMap_apply, fderivWithin_continuousMultilinearMapCompContinuousLinearMap, integral_apply, fderiv_continuousMultilinearMapCompContinuousLinearMap, hasStrictFDerivAt_compContinuousLinearMap, HasStrictFDerivAt.continuousMultilinearMapCompContinuousLinearMap, cpolynomialOn_uncurry_compContinuousLinearMap, analyticWithinAt_uncurry_compContinuousLinearMap, VectorFourier.fourierIntegral_continuousMultilinearMap_apply, Real.fourier_continuousMultilinearMap_apply, analyticOnNhd_uncurry_compContinuousLinearMap, cpolynomialAt_uncurry_compContinuousLinearMap, analyticOn_uncurry_compContinuousLinearMap, Real.fourierIntegral_continuousMultilinearMap_apply'
normedAddCommGroup' 📖	CompOp	59 math math: FormalMultilinearSeries.hasFiniteFPowerSeriesOnBall_changeOrigin, AnalyticOn.exists_hasFTaylorSeriesUpToOn, FormalMultilinearSeries.changeOriginSeries_sum_eq_partialSum_of_finite, ContDiff.iteratedFDeriv_right, ContDiffMapSupportedIn.iteratedFDerivLM_apply, ContDiffMapSupportedIn.structureMapCLM_eq_of_scalars, AnalyticOnNhd.iteratedFDeriv_of_isOpen, ContDiffMapSupportedIn.structureMapCLM_apply, FormalMultilinearSeries.le_changeOriginSeries_radius, AnalyticOn.iteratedFDerivWithin, ContDiffMapSupportedIn.iteratedFDerivWithOrderLM_apply_of_gt, OrderedFinpartition.norm_compAlongOrderedFinpartitionL_apply_le, AnalyticOnNhd.iteratedFDeriv, ContDiffMapSupportedIn.iteratedFDerivWithOrderLM_eq_of_scalars, Real.fourier_iteratedFDeriv, iteratedFDeriv_sum, VectorFourier.fourierIntegral_iteratedFDeriv, VectorFourier.norm_iteratedFDeriv_fourierPowSMulRight, ContDiffMapSupportedIn.structureMapLM_eq_of_scalars, ContDiffAt.iteratedFDeriv_right, CPolynomialOn.iteratedFDeriv, ContDiffMapSupportedIn.uniformSpace_eq_iInf, contDiffWithinAt_iff_of_ne_infty, VectorFourier.iteratedFDeriv_fourierIntegral, ContDiffMapSupportedIn.continuous_iff_comp_withOrder, ContDiffMapSupportedIn.structureMapCLM_zero_apply, ContDiffMapSupportedIn.iteratedFDerivWithOrderLM_apply, ContDiffMapSupportedIn.structureMapLM_apply_withOrder, FormalMultilinearSeries.cpolynomialAt_changeOrigin_of_finite, VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral', ContDiffMapSupportedIn.isUniformEmbedding_pi_structureMapCLM, ContDiff.fourierPowSMulRight, OrderedFinpartition.compAlongOrderedFinpartitionL_apply, ContDiffMapSupportedIn.structureMapCLM_apply_withOrder, ContDiffMapSupportedIn.seminorm_apply, Real.iteratedFDeriv_fourier, ContDiff.iteratedFDeriv_right', FormalMultilinearSeries.analyticAt_changeOrigin, HasFPowerSeriesWithinOnBall.iteratedFDerivWithin, ContDiffWithinAt.iteratedFDerivWithin_right, ContDiffMapSupportedIn.structureMapLM_zero_injective, OrderedFinpartition.norm_compAlongOrderedFinpartition_sub_compAlongOrderedFinpartition_le, VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral, Real.iteratedFDeriv_fourierIntegral, iteratedFDerivWithin_sum_apply, ContDiffMapSupportedIn.continuous_iff_comp, VectorFourier.fourierPowSMulRight_iteratedFDeriv_fourierIntegral, ContDiffPointwiseHolderAt.iteratedFDeriv, ContDiffMapSupportedIn.structureMapCLM_zero_injective, ContDiffMapSupportedIn.iteratedFDerivLM_eq_of_scalars, ContDiffMapSupportedIn.structureMapLM_zero_apply, VectorFourier.norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le, Real.fourierIntegral_iteratedFDeriv, ContDiffMapSupportedIn.structureMapLM_apply, FormalMultilinearSeries.hasFPowerSeriesOnBall_changeOrigin, ContDiffMapSupportedIn.structureMapLM_eq, OrderedFinpartition.norm_compAlongOrderedFinpartitionL_le, ContDiffMapSupportedIn.iteratedFDerivWithOrderLM_apply_of_le, AnalyticWithinAt.exists_hasFTaylorSeriesUpToOn
normedSpace 📖	CompOp	37 math math: fderiv_iteratedFDeriv, analyticAt_uncurry_compContinuousLinearMap, norm_compContinuousLinearMapLRight_le, iteratedFDerivWithin_succ_eq_comp_left, norm_smulRightL_le, Real.fourierIntegral_continuousMultilinearMap_apply, curryLeft_norm, fderivWithin_iteratedFDerivWithin, MultilinearMap.mkContinuousLinear_norm_le, PiTensorProduct.dualSeminorms_bounded, curryMidEquiv_apply, ContinuousLinearMap.norm_map_tail_le, PiTensorProduct.injectiveSeminorm_apply, MultilinearMap.mkContinuousLinear_norm_le', integral_apply, ContinuousLinearMap.norm_uncurryMid, ContinuousLinearMap.uncurryLeft_norm, MultilinearMap.mkContinuousMultilinear_norm_le', continuousMultilinearCurryLeftEquiv_apply, MultilinearMap.mkContinuousMultilinear_norm_le, PiTensorProduct.toDualContinuousMultilinearMap_le_projectiveSeminorm, cpolynomialOn_uncurry_compContinuousLinearMap, analyticWithinAt_uncurry_compContinuousLinearMap, VectorFourier.fourierIntegral_continuousMultilinearMap_apply, Real.fourier_continuousMultilinearMap_apply, analyticOnNhd_uncurry_compContinuousLinearMap, continuousMultilinearCurryLeftEquiv_symm_apply, iteratedFDeriv_succ_eq_comp_left, cpolynomialAt_uncurry_compContinuousLinearMap, norm_compContinuousLinearMapL_le, analyticOn_uncurry_compContinuousLinearMap, ContinuousLinearMap.norm_map_removeNth_le, Real.fourierIntegral_continuousMultilinearMap_apply', norm_curryMid, PiTensorProduct.injectiveSeminorm_def, OrderedFinpartition.norm_compAlongOrderedFinpartitionL_le, curryMidEquiv_symm_apply
normedSpace' 📖	CompOp	50 math math: FormalMultilinearSeries.hasFiniteFPowerSeriesOnBall_changeOrigin, AnalyticOn.exists_hasFTaylorSeriesUpToOn, ContDiff.iteratedFDeriv_right, ContDiffMapSupportedIn.iteratedFDerivLM_apply, AnalyticOnNhd.iteratedFDeriv_of_isOpen, FormalMultilinearSeries.le_changeOriginSeries_radius, AnalyticOn.iteratedFDerivWithin, FormalMultilinearSeries.changeOriginSeries_summable_aux₃, ContDiffMapSupportedIn.iteratedFDerivWithOrderLM_apply_of_gt, OrderedFinpartition.norm_compAlongOrderedFinpartitionL_apply_le, AnalyticOnNhd.iteratedFDeriv, ContDiffMapSupportedIn.iteratedFDerivWithOrderLM_eq_of_scalars, Real.fourier_iteratedFDeriv, FormalMultilinearSeries.nnnorm_changeOriginSeries_le_tsum, VectorFourier.fourierIntegral_iteratedFDeriv, VectorFourier.norm_iteratedFDeriv_fourierPowSMulRight, curryFinFinset_symm_apply_const, ContDiffAt.iteratedFDeriv_right, CPolynomialOn.iteratedFDeriv, contDiffWithinAt_iff_of_ne_infty, VectorFourier.iteratedFDeriv_fourierIntegral, ContDiffMapSupportedIn.iteratedFDerivWithOrderLM_apply, curryFinFinset_apply_const, FormalMultilinearSeries.cpolynomialAt_changeOrigin_of_finite, norm_fderiv_iteratedFDeriv, norm_fderivWithin_iteratedFDerivWithin, VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral', ContDiff.fourierPowSMulRight, curryFinFinset_symm_apply_piecewise_const, Real.iteratedFDeriv_fourier, ContDiff.iteratedFDeriv_right', FormalMultilinearSeries.analyticAt_changeOrigin, HasFPowerSeriesWithinOnBall.iteratedFDerivWithin, ContDiffWithinAt.iteratedFDerivWithin_right, VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral, Real.iteratedFDeriv_fourierIntegral, VectorFourier.fourierPowSMulRight_iteratedFDeriv_fourierIntegral, ContDiffPointwiseHolderAt.iteratedFDeriv, FormalMultilinearSeries.norm_changeOriginSeriesTerm, curryFinFinset_symm_apply, FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm, ContDiffMapSupportedIn.iteratedFDerivLM_eq_of_scalars, curryFinFinset_apply, VectorFourier.norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le, Real.fourierIntegral_iteratedFDeriv, FormalMultilinearSeries.hasFPowerSeriesOnBall_changeOrigin, ContDiffMapSupportedIn.structureMapLM_eq, OrderedFinpartition.norm_compAlongOrderedFinpartitionL_le, ContDiffMapSupportedIn.iteratedFDerivWithOrderLM_apply_of_le, AnalyticWithinAt.exists_hasFTaylorSeriesUpToOn
ofSubsingletonₗᵢ 📖	CompOp	2 math math: ofSubsingletonₗᵢ_symm_apply, ofSubsingletonₗᵢ_apply
opNorm 📖	CompOp	—
piFieldEquiv 📖	CompOp	4 math math: iteratedFDerivWithin_eq_equiv_comp, iteratedFDeriv_eq_equiv_comp, iteratedDeriv_eq_equiv_comp, iteratedDerivWithin_eq_equiv_comp
piₗᵢ 📖	CompOp	2 math math: piₗᵢ_symm_apply, piₗᵢ_apply
prodL 📖	CompOp	2 math math: prodL_apply, prodL_symm_apply
restr 📖	CompOp	1 math math: norm_restr
restrictScalarsₗᵢ 📖	CompOp	—
seminorm 📖	CompOp	—
seminormedAddCommGroup 📖	CompOp	52 math math: fderiv_iteratedFDeriv, norm_compContinuousLinearMapLRight_le, iteratedFDerivWithin_succ_eq_comp_left, PiTensorProduct.toDualContinuousMultilinearMap_apply_apply, norm_smulRightL_le, VectorFourier.fourierPowSMulRight_eq_comp, nnnorm_constOfIsEmpty, curryLeft_norm, isBoundedBilinearMap_compMultilinear, PiTensorProduct.liftIsometry_tprodL, continuousMultilinearCurryRightEquiv_symm_apply, prodL_apply, ContinuousLinearMap.coe_flipMultilinearEquiv, fderivWithin_iteratedFDerivWithin, MultilinearMap.mkContinuousLinear_norm_le, opNorm_pi, PiTensorProduct.dualSeminorms_bounded, curryMidEquiv_apply, isLeast_opNNNorm, ContinuousLinearMap.norm_map_tail_le, PiTensorProduct.injectiveSeminorm_apply, MultilinearMap.mkContinuousLinear_norm_le', ContinuousLinearMap.norm_uncurryMid, ContinuousLinearMap.uncurryLeft_norm, MultilinearMap.mkContinuousMultilinear_norm_le', opNNNorm_prod, PiTensorProduct.liftIsometry_comp_mapL, continuousMultilinearCurryLeftEquiv_apply, PiTensorProduct.liftIsometry_symm_apply, piₗᵢ_symm_apply, MultilinearMap.mkContinuousMultilinear_norm_le, opNNNorm_pi, PiTensorProduct.toDualContinuousMultilinearMap_le_projectiveSeminorm, PiTensorProduct.liftIsometry_apply_apply, prodL_symm_apply, opNNNorm_le_iff, ContinuousLinearMap.coe_symm_flipMultilinearEquiv, continuousMultilinearCurryLeftEquiv_symm_apply, smulRightL_apply, iteratedFDeriv_succ_eq_comp_left, piₗᵢ_apply, nnnorm_smulRight, le_opNNNorm, norm_compContinuousLinearMapL_le, continuousMultilinearCurryRightEquiv_apply, ContinuousLinearMap.norm_map_removeNth_le, compContinuousLinearMapContinuousMultilinear_apply_apply, isBoundedLinearMap_prod_multilinear, norm_curryMid, PiTensorProduct.injectiveSeminorm_def, OrderedFinpartition.norm_compAlongOrderedFinpartitionL_le, curryMidEquiv_symm_apply
seminormedAddCommGroup' 📖	CompOp	98 math math: hasFTaylorSeriesUpToOn_top_iff_right, ContDiffMapSupportedIn.structureMapCLM_eq_of_scalars, changeOrigin_toFormalMultilinearSeries, ContDiffMapSupportedIn.structureMapCLM_apply, iteratedFDerivWithin_succ_eq_comp_right, HasFTaylorSeriesUpTo.hasFDerivAt, FormalMultilinearSeries.changeOriginSeries_summable_aux₃, HasFPowerSeriesWithinAt.hasStrictFDerivWithinAt, OrderedFinpartition.norm_compAlongOrderedFinpartitionL_apply_le, HasFTaylorSeriesUpToOn.zero_eq', FormalMultilinearSeries.nnnorm_mul_pow_le_of_lt_radius, FormalMultilinearSeries.nnnorm_changeOrigin_le, FormalMultilinearSeries.nnnorm_changeOriginSeries_le_tsum, HasFTaylorSeriesUpToOn.eventually_hasFDerivAt, VectorFourier.norm_iteratedFDeriv_fourierPowSMulRight, curryFinFinset_symm_apply_const, HasFPowerSeriesOnBall.fderiv_eq, HasFTaylorSeriesUpToOn.hasFDerivWithinAt, ContDiffMapSupportedIn.structureMapLM_eq_of_scalars, HasFPowerSeriesWithinAt.fderivWithin_eq, FormalMultilinearSeries.compAlongComposition_nnnorm, ContDiffMapSupportedIn.uniformSpace_eq_iInf, ContDiffMapSupportedIn.continuous_iff_comp_withOrder, iteratedFDerivWithin_eq_equiv_comp, ContDiffMapSupportedIn.structureMapCLM_zero_apply, FormalMultilinearSeries.nnnorm_compContinuousLinearMap_le, ofSubsingletonₗᵢ_symm_apply, continuousMultilinearCurryFin0_symm_apply, FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm_apply_le, ContinuousAlternatingMap.toContinuousMultilinearMapLI_apply, FormalMultilinearSeries.radius_inv_eq_limsup, hasFTaylorSeriesUpToOn_succ_iff_right, FormalMultilinearSeries.nnnorm_changeOriginSeries_apply_le_tsum, ContDiffMapSupportedIn.structureMapLM_apply_withOrder, curryFinFinset_apply_const, hasFTaylorSeriesUpTo_succ_nat_iff_right, iteratedFDeriv_eq_equiv_comp, hasFTaylorSeriesUpToOn_succ_nat_iff_right, HasFPowerSeriesAt.fderiv_eq, continuousMultilinearCurryFin0_apply, norm_fderiv_iteratedFDeriv, HasFTaylorSeriesUpToOn.hasFDerivAt, iteratedDeriv_eq_equiv_comp, norm_fderivWithin_iteratedFDerivWithin, HasFTaylorSeriesUpToOn.shift_of_succ, ContDiffMapSupportedIn.isUniformEmbedding_pi_structureMapCLM, curryFinFinset_symm_apply_piecewise_const, FormalMultilinearSeries.leftInv_coeff_one, HasFPowerSeriesAt.hasFDerivAt, ContDiffMapSupportedIn.structureMapCLM_apply_withOrder, FormalMultilinearSeries.changeOriginSeries_summable_aux₁, iteratedFDeriv_succ_eq_comp_right, ContDiffMapSupportedIn.seminorm_apply, nnnorm_ofSubsingleton, HasFPowerSeriesWithinOnBall.fderivWithin_eq, HasFTaylorSeriesUpToOn.hasStrictFDerivAt, ContinuousAlternatingMap.nnnorm_toContinuousMultilinearMap, HasFPowerSeriesOnBall.hasFDerivAt, FormalMultilinearSeries.changeOriginSeries_summable_aux₂, iteratedFDeriv_zero_eq_comp, continuousMultilinearCurryRightEquiv_symm_apply', ContDiffMapSupportedIn.structureMapLM_zero_injective, iteratedDerivWithin_eq_equiv_comp, nnnorm_ofSubsingleton_id_le, FormalMultilinearSeries.summable_nnnorm_mul_pow, iteratedFDerivWithin_zero_eq_comp, nnnorm_ofSubsingleton_id, HasFiniteFPowerSeriesOnBall.hasStrictFDerivAt, continuousMultilinearCurryRightEquiv_apply', HasFiniteFPowerSeriesOnBall.hasFDerivAt, ContDiffMapSupportedIn.continuous_iff_comp, FormalMultilinearSeries.enorm_compContinuousLinearMap_le, VectorFourier.fourierPowSMulRight_iteratedFDeriv_fourierIntegral, ContDiffMapSupportedIn.structureMapCLM_zero_injective, ofSubsingletonₗᵢ_apply, continuousMultilinearCurryFin1_symm_apply, FormalMultilinearSeries.norm_changeOriginSeriesTerm, HasFTaylorSeriesUpTo.zero_eq', curryFinFinset_symm_apply, HasFiniteFPowerSeriesOnBall.fderiv_eq, HasFPowerSeriesAt.hasStrictFDerivAt, isBoundedLinearMap_continuousMultilinearMap_comp_linear, FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm, ContDiffMapSupportedIn.structureMapLM_zero_apply, HasFPowerSeriesWithinAt.hasFDerivWithinAt, VectorFourier.integrable_fourierPowSMulRight, FormalMultilinearSeries.rightInv_coeff_one, ContinuousAlternatingMap.enorm_toContinuousMultilinearMap, ContinuousLinearMap.fpowerSeries_apply_one, curryFinFinset_apply, VectorFourier.norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le, FormalMultilinearSeries.radius_eq_liminf, HasFPowerSeriesWithinOnBall.hasFDerivWithinAt, ContDiffMapSupportedIn.structureMapLM_apply, ContinuousLinearMap.fpowerSeriesBilinear_apply_one, OrderedFinpartition.norm_compAlongOrderedFinpartitionL_le, FormalMultilinearSeries.comp_summable_nnreal, continuousMultilinearCurryFin1_apply
smulRightL 📖	CompOp	3 math math: norm_smulRightL_le, VectorFourier.fourierPowSMulRight_eq_comp, smulRightL_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bounds_bddBelow 📖	mathematical	—	BddBelow Real Real.instLE setOf Real.instZero	—	—
bounds_nonempty 📖	mathematical	—	Real Set Set.instMembership setOf Real.instLE Real.instZero	—	bound le_of_lt
compContinuousLinearMapContinuousMultilinear_apply_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ContinuousMultilinearMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instTopologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction 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 smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.funLike ContinuousLinearMap.addCommMonoid seminormedAddCommGroup instIsTopologicalAddGroup ContinuousLinearMap.module SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instSMulCommClass instContinuousConstSMul ContinuousLinearMap.topologicalSpace instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing funLike compContinuousLinearMapContinuousMultilinear compContinuousLinearMap	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self instIsTopologicalAddGroup instSMulCommClass instContinuousConstSMul
compContinuousLinearMapLRight_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup addCommMonoid ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction MonoidWithZero.toMonoid Semiring.toMonoidWithZero SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Module.toDistribMulAction UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass DistribMulAction.toDistribSMul IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toIsBoundedSMul instModule AddZero.toZero AddZeroClass.toAddZero AddCommMonoid.toAddMonoid CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.topologicalSpace instTopologicalSpace funLike compContinuousLinearMapLRight compContinuousLinearMap	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
compContinuousLinearMapL_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ContinuousMultilinearMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instTopologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction 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 smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.funLike compContinuousLinearMapL compContinuousLinearMap	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self
fderivCompContinuousLinearMap_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace funLike ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring Pi.topologicalSpace ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup Pi.addCommMonoid ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup instTopologicalSpace addCommMonoid Pi.module ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction MonoidWithZero.toMonoid Semiring.toMonoidWithZero SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Module.toDistribMulAction UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass DistribMulAction.toDistribSMul IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toIsBoundedSMul instModule AddZero.toZero AddZeroClass.toAddZero AddCommMonoid.toAddMonoid CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.funLike fderivCompContinuousLinearMap Finset.sum Finset.univ Function.update	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul linearDeriv_apply Finset.sum_congr ContinuousLinearMap.compContinuousMultilinearMap_coe sum_apply
flipLinear_apply_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace funLike ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring instTopologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction 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 smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.funLike flipLinear ContinuousLinearMap.addCommMonoid ContinuousLinearMap.module ContinuousLinearMap.topologicalSpace	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
flipMultilinear_flipLinear 📖	mathematical	—	ContinuousLinearMap.flipMultilinear flipLinear	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
instContinuousEval 📖	mathematical	—	ContinuousEval ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace funLike instTopologicalSpace Pi.topologicalSpace	—	nonempty_fintype isUniformAddGroup_of_addCommGroup ContinuousOn.comp_continuous IsUniformAddGroup.to_topologicalAddGroup UniformOnFun.continuousOn_eval₂ NormedSpace.isVonNBounded_of_isBounded Metric.isBounded_ball Metric.ball_mem_nhds one_pos Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Continuous.prodMap Topology.IsEmbedding.continuous isEmbedding_toUniformOnFun continuous_id Continuous.continuousAt cont
instIsBoundedSMul 📖	mathematical	—	IsBoundedSMul ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedRing.toPseudoMetricSpace instPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedRing.toRing instZero instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring AddCommMonoid.toAddMonoid Module.toDistribMulAction UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsBoundedSMul.toUniformContinuousConstSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	IsBoundedSMul.of_norm_smul_le SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul opNorm_smul_le
isLeast_opNNNorm 📖	mathematical	—	IsLeast NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal setOf NNNorm.nnnorm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup	—	isLeast_Ici
isLeast_opNorm 📖	mathematical	—	IsLeast Real Real.instLE setOf Real.instZero Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace hasOpNorm	—	IsClosed.isLeast_csInf instOrderTopologyReal Set.setOf_forall IsClosed.inter isClosed_Ici instClosedIciTopology OrderTopology.to_orderClosedTopology isClosed_iInter isClosed_le continuous_const Continuous.comp' Continuous.fun_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Continuous.fst continuous_id' Continuous.snd Continuous.prodMk bounds_nonempty bounds_bddBelow
iteratedFDerivComponent_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Pi.addCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Pi.module NormedSpace.toModule Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace funLike Set Set.instMembership addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction 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 smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing instTopologicalSpace Pi.addCommGroup iteratedFDerivComponent Equiv Set.Elem EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self MultilinearMap.mkContinuousMultilinear.congr_simp
le_mul_prod_of_opNorm_le_of_le 📖	mathematical	Real Real.instLE Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace hasOpNorm SeminormedAddCommGroup.toNorm	DFunLike.coe funLike Real.instMul Finset.prod Real.instCommMonoid Finset.univ	—	LE.le.trans le_opNorm mul_le_mul IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono Finset.prod_le_prod Real.instZeroLEOneClass norm_nonneg Finset.prod_nonneg opNorm_nonneg
le_of_opNNNorm_le 📖	mathematical	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup	DFunLike.coe funLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Finset.prod CommSemiring.toCommMonoid instCommSemiringNNReal Finset.univ	—	LE.le.trans le_opNNNorm mul_le_mul' NNReal.mulLeftMono covariant_swap_mul_of_covariant_mul le_rfl
le_of_opNorm_le 📖	mathematical	Real Real.instLE Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace hasOpNorm	SeminormedAddCommGroup.toNorm DFunLike.coe funLike Real.instMul Finset.prod Real.instCommMonoid Finset.univ	—	le_mul_prod_of_opNorm_le_of_le le_rfl
le_opNNNorm 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace funLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal seminormedAddCommGroup Finset.prod CommSemiring.toCommMonoid instCommSemiringNNReal Finset.univ	—	NNReal.coe_le_coe NNReal.coe_prod Finset.prod_congr le_opNorm
le_opNorm 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace funLike Real.instMul hasOpNorm Finset.prod Real.instCommMonoid Finset.univ	—	isLeast_opNorm
le_opNorm_mul_pow_card_of_le 📖	mathematical	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm Pi.seminormedAddCommGroup	DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace funLike Real.instMul hasOpNorm Monoid.toNatPow Real.instMonoid Fintype.card	—	Finset.prod_const le_opNorm_mul_prod_of_le LE.le.trans norm_le_pi_norm
le_opNorm_mul_pow_of_le 📖	mathematical	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm Pi.seminormedAddCommGroup Fin.fintype	DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace funLike Real.instMul hasOpNorm Monoid.toNatPow Real.instMonoid	—	Fintype.card_fin le_opNorm_mul_pow_card_of_le
le_opNorm_mul_prod_of_le 📖	mathematical	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm	DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace funLike Real.instMul hasOpNorm Finset.prod Real.instCommMonoid Finset.univ	—	le_mul_prod_of_opNorm_le_of_le le_rfl
nnnorm_constOfIsEmpty 📖	mathematical	—	NNNorm.nnnorm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup constOfIsEmpty	—	NNReal.eq norm_constOfIsEmpty
nnnorm_ofSubsingleton 📖	mathematical	—	NNNorm.nnnorm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup' DFunLike.coe Equiv ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike ofSubsingleton ContinuousLinearMap.toSeminormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	—	NNReal.eq RingHomIsometric.ids norm_ofSubsingleton
nnnorm_ofSubsingleton_id 📖	mathematical	—	NNNorm.nnnorm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup' DFunLike.coe Equiv ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike ofSubsingleton ContinuousLinearMap.id NNReal instOneNNReal	—	NNReal.eq norm_ofSubsingleton_id
nnnorm_ofSubsingleton_id_le 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup' DFunLike.coe Equiv ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike ofSubsingleton ContinuousLinearMap.id instOneNNReal	—	norm_ofSubsingleton_id_le
nnnorm_smulRight 📖	mathematical	—	NNNorm.nnnorm ContinuousMultilinearMap CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup smulRight SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing IsBoundedSMul.continuousSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NormedSpace.toIsBoundedSMul NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal DivisionSemiring.toSemiring Semifield.toDivisionSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace	—	le_antisymm IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul opNNNorm_le_iff LE.le.trans nnnorm_smul_le mul_right_comm mul_le_mul_left covariant_swap_mul_of_covariant_mul NNReal.mulLeftMono le_opNNNorm eq_zero_or_pos NNReal.instCanonicallyOrderedAdd MulZeroClass.mul_zero le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono NNReal.instIsStrictOrderedRing div_mul_eq_mul_div le_trans smulRight_apply nnnorm_smul NormedSpace.toNormSMulClass le_refl
norm_compContinuousLinearMapLRight_le 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousMultilinearMap ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup addCommMonoid ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction MonoidWithZero.toMonoid Semiring.toMonoidWithZero SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Module.toDistribMulAction UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass DistribMulAction.toDistribSMul IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toIsBoundedSMul instModule AddZero.toZero AddZeroClass.toAddZero AddCommMonoid.toAddMonoid CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.topologicalSpace instTopologicalSpace hasOpNorm ContinuousLinearMap.toSeminormedAddCommGroup RingHomIsometric.ids ContinuousLinearMap.toNormedSpace seminormedAddCommGroup normedSpace compContinuousLinearMapLRight	—	MultilinearMap.mkContinuous_norm_le norm_nonneg
norm_compContinuousLinearMapL_le 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ContinuousMultilinearMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instTopologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction 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 smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.hasOpNorm seminormedAddCommGroup normedSpace compContinuousLinearMapL Finset.prod Real.instCommMonoid Finset.univ	—	LinearMap.mkContinuous_norm_le smulCommClass_self Finset.prod_nonneg Real.instZeroLEOneClass IsOrderedRing.toPosMulMono Real.instIsOrderedRing norm_nonneg RingHomIsometric.ids
norm_compContinuousLinearMap_le 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace hasOpNorm compContinuousLinearMap Real.instMul Finset.prod Real.instCommMonoid Finset.univ ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.hasOpNorm	—	opNorm_le_bound mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing norm_nonneg Finset.prod_nonneg Real.instZeroLEOneClass RingHomIsometric.ids le_opNorm mul_le_mul_of_nonneg_left Finset.prod_le_prod ContinuousLinearMap.le_opNorm Finset.prod_mul_distrib mul_assoc
norm_compContinuous_linearIsometryEquiv 📖	mathematical	—	Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace hasOpNorm compContinuousLinearMap ContinuousLinearEquiv.toContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearIsometryEquiv.toContinuousLinearEquiv	—	RingHomInvPair.ids le_antisymm norm_compContinuous_linearIsometry_le ext LinearIsometryEquiv.apply_symm_apply
norm_compContinuous_linearIsometry_le 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace hasOpNorm compContinuousLinearMap LinearIsometry.toContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring	—	opNorm_le_bound norm_nonneg LE.le.trans le_opNorm Finset.prod_congr LinearIsometry.norm_map
norm_constOfIsEmpty 📖	mathematical	—	Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace hasOpNorm constOfIsEmpty SeminormedAddCommGroup.toNorm	—	le_antisymm opNorm_le_bound norm_nonneg Fintype.prod_empty mul_one constOfIsEmpty_apply le_refl Finset.prod_congr Finset.univ_eq_empty norm_zero Finset.prod_const pow_zero le_opNorm
norm_def 📖	mathematical	—	Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace hasOpNorm InfSet.sInf Real Real.instInfSet setOf Real.instLE Real.instZero	—	—
norm_image_sub_le 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace funLike Real.instMul hasOpNorm Real.instNatCast Fintype.card Monoid.toNatPow Real.instMonoid Real.instMax Pi.seminormedAddCommGroup Pi.instSub	—	MultilinearMap.norm_image_sub_le_of_bound norm_nonneg le_opNorm
norm_image_sub_le' 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace funLike Real.instMul hasOpNorm Finset.sum Real.instAddCommMonoid Finset.univ Finset.prod Real.instCommMonoid Real.instMax	—	MultilinearMap.norm_image_sub_le_of_bound' norm_nonneg le_opNorm
norm_iteratedFDerivComponent_le 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Pi.addCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Pi.module NormedSpace.toModule Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace hasOpNorm' Pi.seminormedAddCommGroup Pi.normedSpace DFunLike.coe Set Set.instMembership addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction 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 smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing instTopologicalSpace Pi.addCommGroup funLike iteratedFDerivComponent Real.instMul hasOpNorm Monoid.toNatPow Real.instMonoid SeminormedAddCommGroup.toNorm Fintype.card	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self le_opNorm mul_le_mul IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono MultilinearMap.mkContinuousMultilinear_norm_le norm_nonneg Finset.prod_le_prod Real.instZeroLEOneClass norm_le_pi_norm Finset.prod_nonneg Finset.prod_const Finset.card_univ Fintype.card_subtype_compl Fintype.card_ofFinset Fintype.card_congr
norm_iteratedFDeriv_le' 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Pi.addCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Pi.module NormedSpace.toModule Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace hasOpNorm' Pi.seminormedAddCommGroup Pi.normedSpace Fin.fintype iteratedFDeriv Real.instMul Real.instNatCast Nat.descFactorial Fintype.card hasOpNorm Monoid.toNatPow Real.instMonoid SeminormedAddCommGroup.toNorm	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self norm_sum_le Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Fintype.card_fin norm_iteratedFDerivComponent_le Finset.sum_const Fintype.card_embedding_eq nsmul_eq_mul mul_assoc
norm_mkPiAlgebra 📖	mathematical	—	Norm.norm ContinuousMultilinearMap CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommRing.toCommSemiring NormedCommRing.toCommRing Algebra.toModule NormedAlgebra.toAlgebra SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace hasOpNorm' NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace mkPiAlgebra IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NonUnitalSeminormedRing.toIsTopologicalRing Real Real.instOne	—	isEmpty_or_nonempty IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing norm_mkPiAlgebra_of_empty NormOneClass.norm_one le_antisymm norm_mkPiAlgebra_le Finset.prod_const_one Finset.prod_congr div_self NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing ratio_le_opNorm
norm_mkPiAlgebraFin 📖	mathematical	—	Norm.norm ContinuousMultilinearMap CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing Algebra.toModule NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace hasOpNorm' NonUnitalSeminormedRing.toSeminormedAddCommGroup SeminormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace Fin.fintype mkPiAlgebraFin IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalSeminormedRing.toIsTopologicalRing Real Real.instOne	—	IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing norm_mkPiAlgebraFin_zero NormOneClass.norm_one le_antisymm norm_mkPiAlgebraFin_succ_le List.ofFn_const List.prod_replicate one_pow mul_one Finset.prod_congr Finset.prod_const_one div_self NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing ratio_le_opNorm
norm_mkPiAlgebraFin_le 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousMultilinearMap CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing Algebra.toModule NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace hasOpNorm' NonUnitalSeminormedRing.toSeminormedAddCommGroup SeminormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace Fin.fintype mkPiAlgebraFin IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalSeminormedRing.toIsTopologicalRing Real.instMax Real.instOne SeminormedRing.toNorm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing LE.le.trans Eq.le norm_mkPiAlgebraFin_zero le_max_right norm_mkPiAlgebraFin_le_of_pos le_max_left
norm_mkPiAlgebraFin_le_of_pos 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousMultilinearMap CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing Algebra.toModule NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace hasOpNorm' NonUnitalSeminormedRing.toSeminormedAddCommGroup SeminormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace Fin.fintype mkPiAlgebraFin IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalSeminormedRing.toIsTopologicalRing Real.instOne	—	IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing LT.lt.ne' norm_mkPiAlgebraFin_succ_le
norm_mkPiAlgebraFin_succ_le 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousMultilinearMap CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing Algebra.toModule NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace hasOpNorm' NonUnitalSeminormedRing.toSeminormedAddCommGroup SeminormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace Fin.fintype mkPiAlgebraFin IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalSeminormedRing.toIsTopologicalRing Real.instOne	—	opNorm_le_bound IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing zero_le_one Real.instZeroLEOneClass List.ofFn_eq_map Fin.prod_univ_def one_mul LE.le.trans_eq List.norm_prod_le'
norm_mkPiAlgebraFin_zero 📖	mathematical	—	Norm.norm ContinuousMultilinearMap CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ring.toSemiring SeminormedRing.toRing Algebra.toModule NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace hasOpNorm' NonUnitalSeminormedRing.toSeminormedAddCommGroup SeminormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace Fin.fintype mkPiAlgebraFin IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalSeminormedRing.toIsTopologicalRing SeminormedRing.toNorm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	le_antisymm IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing opNorm_le_bound norm_nonneg Finset.prod_congr Finset.univ_eq_empty Fin.isEmpty' mul_one Finset.prod_const pow_zero div_one ratio_le_opNorm
norm_mkPiAlgebra_le 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousMultilinearMap CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommRing.toCommSemiring NormedCommRing.toCommRing Algebra.toModule NormedAlgebra.toAlgebra SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace hasOpNorm' NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace mkPiAlgebra IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NonUnitalSeminormedRing.toIsTopologicalRing Real.instOne	—	opNorm_le_bound IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing zero_le_one Real.instZeroLEOneClass one_mul Finset.norm_prod_le' Finset.univ_nonempty
norm_mkPiAlgebra_of_empty 📖	mathematical	—	Norm.norm ContinuousMultilinearMap CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommRing.toCommSemiring NormedCommRing.toCommRing Algebra.toModule NormedAlgebra.toAlgebra SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace hasOpNorm' NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace mkPiAlgebra IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NonUnitalSeminormedRing.toIsTopologicalRing NormedRing.toNorm NormedCommRing.toNormedRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing	—	le_antisymm IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing opNorm_le_bound Finset.prod_congr Finset.univ_eq_empty mul_one Finset.prod_const_one Finset.prod_const pow_zero div_one ratio_le_opNorm
norm_mkPiRing 📖	mathematical	—	Norm.norm ContinuousMultilinearMap CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing NormedField.toField NontriviallyNormedField.toNormedField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Semiring.toModule NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SeminormedAddCommGroup.toPseudoMetricSpace hasOpNorm' NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace mkPiRing IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing IsBoundedSMul.continuousSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toNorm	—	IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul mkPiRing.eq_1 norm_smulRight NonUnitalSeminormedRing.toIsTopologicalRing norm_mkPiAlgebra NormedDivisionRing.to_normOneClass one_mul
norm_ofSubsingleton 📖	mathematical	—	Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace hasOpNorm' DFunLike.coe Equiv ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike ofSubsingleton ContinuousLinearMap.hasOpNorm	—	Finset.prod_congr Finset.univ_unique Finset.prod_singleton Function.Surjective.forall Equiv.surjective
norm_ofSubsingleton_id 📖	mathematical	—	Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule hasOpNorm' DFunLike.coe Equiv ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike ofSubsingleton ContinuousLinearMap.id Real Real.instOne	—	norm_ofSubsingleton ContinuousLinearMap.norm_id EMetric.instNontrivialTopologyOfNontrivial
norm_ofSubsingleton_id_le 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace hasOpNorm' DFunLike.coe Equiv ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike ofSubsingleton ContinuousLinearMap.id Real.instOne	—	norm_ofSubsingleton ContinuousLinearMap.norm_id_le
norm_restr 📖	mathematical	Finset.card	Real Real.instLE Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace hasOpNorm' Fin.fintype restr Real.instMul Monoid.toNatPow Real.instMonoid SeminormedAddCommGroup.toNorm	—	MultilinearMap.mkContinuous_norm_le mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing norm_nonneg pow_nonneg Real.instZeroLEOneClass
norm_restrictScalars 📖	mathematical	IsScalarTower Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedAlgebra.toAlgebra SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule	Norm.norm ContinuousMultilinearMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace hasOpNorm restrictScalars	—	—
norm_smulRight 📖	mathematical	—	Norm.norm ContinuousMultilinearMap CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace hasOpNorm smulRight SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing IsBoundedSMul.continuousSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NormedSpace.toIsBoundedSMul Real Real.instMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace SeminormedAddCommGroup.toNorm	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul nnnorm_smulRight
norm_smulRightL_le 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ContinuousMultilinearMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace SeminormedAddCommGroup.toPseudoMetricSpace instTopologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.topologicalSpace instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing instIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid seminormedAddCommGroup Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.to_smulCommClass Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id ContinuousLinearMap.module instSMulCommClass instContinuousConstSMul ContinuousLinearMap.hasOpNorm ContinuousLinearMap.toSeminormedAddCommGroup normedSpace RingHomIsometric.ids ContinuousLinearMap.toNormedSpace smulRightL Real.instOne	—	LinearMap.mkContinuous₂_norm_le zero_le_one Real.instZeroLEOneClass
ofSubsingletonₗᵢ_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousLinearMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousMultilinearMap ContinuousLinearMap.toSeminormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing seminormedAddCommGroup' 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 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 SeminormedAddCommGroup.toIsTopologicalAddGroup instModule EquivLike.toFunLike LinearIsometryEquiv.instEquivLike ofSubsingletonₗᵢ Equiv.toFun ofSubsingleton	—	RingHomInvPair.ids RingHomIsometric.ids smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup
ofSubsingletonₗᵢ_symm_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousLinearMap seminormedAddCommGroup' ContinuousLinearMap.toSeminormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instModule SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace 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 smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.module EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm ofSubsingletonₗᵢ Equiv.invFun ofSubsingleton	—	RingHomInvPair.ids RingHomIsometric.ids SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self
opNNNorm_le_iff 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup DFunLike.coe funLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Finset.prod CommSemiring.toCommMonoid instCommSemiringNNReal Finset.univ	—	opNorm_le_iff NNReal.coe_nonneg NNReal.coe_prod Finset.prod_congr
opNNNorm_pi 📖	mathematical	—	NNNorm.nnnorm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Pi.addCommMonoid NormedSpace.toModule Pi.module UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Pi.topologicalSpace SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup Pi.seminormedAddCommGroup Pi.normedSpace pi Pi.seminormedAddGroup	—	eq_of_forall_ge_iff forall_swap
opNNNorm_prod 📖	mathematical	—	NNNorm.nnnorm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Prod.instAddCommMonoid NormedSpace.toModule Prod.instModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instTopologicalSpaceProd SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup Prod.seminormedAddCommGroup Prod.normedSpace prod NNReal NNReal.instMax	—	eq_of_forall_ge_iff
opNorm_add_le 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace hasOpNorm instAdd IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup Real.instAdd	—	opNorm_le_bound IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup add_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid opNorm_nonneg add_mul Distrib.rightDistribClass norm_add_le_of_le le_opNorm
opNorm_le_bound 📖	mathematical	Real Real.instLE Real.instZero Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace funLike Real.instMul Finset.prod Real.instCommMonoid Finset.univ	hasOpNorm	—	csInf_le bounds_bddBelow
opNorm_le_iff 📖	mathematical	Real Real.instLE Real.instZero	Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace hasOpNorm SeminormedAddCommGroup.toNorm DFunLike.coe funLike Real.instMul Finset.prod Real.instCommMonoid Finset.univ	—	le_of_opNorm_le opNorm_le_bound
opNorm_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace hasOpNorm	—	Real.sInf_nonneg
opNorm_pi 📖	mathematical	—	Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Pi.addCommMonoid NormedSpace.toModule Pi.module UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Pi.topologicalSpace hasOpNorm Pi.seminormedAddCommGroup Pi.normedSpace pi SeminormedAddCommGroup.toNorm seminormedAddCommGroup	—	opNNNorm_pi
opNorm_prod 📖	mathematical	—	Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Prod.instAddCommMonoid NormedSpace.toModule Prod.instModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instTopologicalSpaceProd hasOpNorm Prod.seminormedAddCommGroup Prod.normedSpace prod Real Real.instMax	—	opNNNorm_prod
opNorm_smul_le 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace hasOpNorm instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing AddCommMonoid.toAddMonoid Module.toDistribMulAction UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real.instMul SeminormedRing.toNorm	—	opNorm_le_bound UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing norm_nonneg opNorm_nonneg smul_apply le_imp_le_of_le_of_le norm_smul_le le_refl mul_assoc mul_le_mul_of_nonneg_left le_opNorm
opNorm_zero 📖	mathematical	—	Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace hasOpNorm instZero Real Real.instZero	—	LE.le.antisymm' opNorm_nonneg opNorm_le_bound le_rfl norm_zero MulZeroClass.zero_mul
opNorm_zero_iff 📖	mathematical	—	Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule hasOpNorm Real Real.instZero instZero	—	LE.le.ge_iff_eq' opNorm_nonneg opNorm_le_iff le_rfl MulZeroClass.zero_mul
piₗᵢ_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Pi.module Pi.topologicalSpace Pi.seminormedAddCommGroup seminormedAddCommGroup Pi.normedSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toIsBoundedSMul smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction instContinuousConstSMulForall SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Pi.smulCommClass EquivLike.toFunLike LinearIsometryEquiv.instEquivLike piₗᵢ pi	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self instContinuousConstSMulForall Pi.smulCommClass
piₗᵢ_symm_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Pi.module Pi.topologicalSpace seminormedAddCommGroup Pi.seminormedAddCommGroup Pi.normedSpace instModule SeminormedAddCommGroup.toIsTopologicalAddGroup instContinuousConstSMulForall SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribMulAction.toDistribSMul Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toIsBoundedSMul Pi.smulCommClass smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm piₗᵢ ContinuousLinearMap.compContinuousMultilinearMap ContinuousLinearMap.proj	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup instContinuousConstSMulForall UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Pi.smulCommClass smulCommClass_self IsTopologicalAddGroup.toContinuousAdd
prodL_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Prod.instAddCommMonoid Prod.instModule instTopologicalSpaceProd Prod.seminormedAddCommGroup seminormedAddCommGroup Prod.normedSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction 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 smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing Prod.continuousConstSMul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Prod.smulCommClass EquivLike.toFunLike LinearIsometryEquiv.instEquivLike prodL Equiv.toFun prodEquiv	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self Prod.continuousConstSMul Prod.smulCommClass
prodL_symm_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousMultilinearMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Prod.instAddCommMonoid NormedSpace.toModule Prod.instModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instTopologicalSpaceProd seminormedAddCommGroup Prod.seminormedAddCommGroup Prod.normedSpace instModule SeminormedAddCommGroup.toIsTopologicalAddGroup Prod.continuousConstSMul SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction UniformContinuousConstSMul.to_continuousConstSMul 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 Prod.smulCommClass smulCommClass_self CommRing.toCommMonoid Field.toCommRing CommMonoid.toMonoid Ring.toSemiring CommRing.toRing addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm prodL Equiv.invFun prodEquiv	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup Prod.continuousConstSMul UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Prod.smulCommClass smulCommClass_self IsTopologicalAddGroup.toContinuousAdd
ratio_le_opNorm 📖	mathematical	—	Real Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace funLike Finset.prod Real.instCommMonoid Finset.univ hasOpNorm	—	div_le_of_le_mul₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Finset.prod_nonneg Real.instZeroLEOneClass IsOrderedRing.toPosMulMono Real.instIsOrderedRing norm_nonneg opNorm_nonneg le_opNorm
smulRightL_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup ContinuousMultilinearMap NormedSpace.toModule instTopologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction 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 smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.funLike ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap.topologicalSpace instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing instIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid seminormedAddCommGroup Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.to_smulCommClass Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id ContinuousLinearMap.module instSMulCommClass instContinuousConstSMul smulRightL smulRight IsBoundedSMul.continuousSMul	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing instIsTopologicalAddGroup Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul Algebra.to_smulCommClass instSMulCommClass instContinuousConstSMul
unit_le_opNorm 📖	mathematical	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm Pi.seminormedAddCommGroup Real.instOne	DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace funLike hasOpNorm	—	LE.le.trans le_opNorm_mul_pow_card_of_le one_pow mul_one

LinearIsometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_compContinuousMultilinearMap 📖	mathematical	—	Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap.hasOpNorm ContinuousLinearMap.compContinuousMultilinearMap toContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring	—	ContinuousLinearMap.compContinuousMultilinearMap_coe norm_map

MultilinearMap

Definitions

Name	Category	Theorems
mkContinuous 📖	CompOp	4 math math: coe_mkContinuous, PiTensorProduct.liftEquiv_symm_apply, mkContinuous_norm_le, mkContinuous_norm_le'
mkContinuousLinear 📖	CompOp	2 math math: mkContinuousLinear_norm_le, mkContinuousLinear_norm_le'
mkContinuousMultilinear 📖	CompOp	3 math math: mkContinuousMultilinear_apply, mkContinuousMultilinear_norm_le', mkContinuousMultilinear_norm_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bound_of_shell 📖	—	Real Real.instLT Real.instZero Real.instOne Norm.norm NormedField.toNorm NontriviallyNormedField.toNormedField Real.instLE SeminormedAddCommGroup.toNorm DFunLike.coe MultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLikeForall Real.instMul Finset.prod Real.instCommMonoid Finset.univ NormedAddCommGroup.toNorm	—	—	bound_of_shell_of_norm_map_coord_zero map_coord_zero norm_eq_zero norm_zero
bound_of_shell_of_continuous 📖	—	Continuous Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe MultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLikeForall Real Real.instLT Real.instZero Real.instOne Norm.norm NormedField.toNorm Real.instLE SeminormedAddCommGroup.toNorm Real.instMul Finset.prod Real.instCommMonoid Finset.univ	—	—	bound_of_shell_of_norm_map_coord_zero norm_map_coord_zero
bound_of_shell_of_norm_map_coord_zero 📖	—	Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe MultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLikeForall Real Real.instZero Real.instLT Real.instOne NormedField.toNorm Real.instLE Real.instMul Finset.prod Real.instCommMonoid Finset.univ	—	—	Finset.prod_eq_zero Finset.mem_univ MulZeroClass.mul_zero le_refl Finset.prod_pos Real.instZeroLEOneClass IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instNontrivial norm_pos_iff map_smul_univ norm_smul NormedSpace.toNormSMulClass norm_prod NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass Finset.prod_congr Finset.prod_mul_distrib mul_left_comm IsOrderedRing.toPosMulMono Real.instIsOrderedRing PosMulStrictMono.toPosMulReflectLE rescale_to_shell_semi_normed
coe_mkContinuous 📖	mathematical	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe MultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLikeForall Real.instMul Finset.prod Real.instCommMonoid Finset.univ	ContinuousMultilinearMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap.funLike mkContinuous	—	—
continuous_of_bound 📖	mathematical	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe MultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLikeForall Real.instMul Finset.prod Real.instCommMonoid Finset.univ	Continuous Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	le_trans zero_le_one Real.instZeroLEOneClass le_max_right LE.le.trans mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing le_max_left Finset.prod_nonneg IsOrderedRing.toPosMulMono norm_nonneg continuous_iff_continuousAt continuousAt_of_locally_lipschitz zero_lt_one NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing dist_eq_norm norm_le_of_mem_closedBall le_of_lt IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le norm_image_sub_le_of_bound mul_le_mul_of_nonneg_left pow_le_pow_left₀ le_max_of_le_left mul_nonneg lt_max_of_lt_right Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Nat.cast_nonneg'
exists_bound_of_continuous 📖	mathematical	Continuous Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe MultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLikeForall	Real Real.instLT Real.instZero Real.instLE Norm.norm SeminormedAddCommGroup.toNorm Real.instMul Finset.prod Real.instCommMonoid Finset.univ	—	isEmpty_or_nonempty add_pos_of_nonneg_of_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid norm_nonneg zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Finset.prod_congr Finset.univ_eq_empty norm_zero Finset.prod_const pow_zero mul_one IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le NormedAddCommGroup.tendsto_nhds_nhds Continuous.tendsto NormedField.exists_one_lt_norm pow_pos IsStrictOrderedRing.toPosMulStrictMono div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LT.lt.trans bound_of_shell_of_continuous LE.le.trans LT.lt.le sub_zero map_zero pi_norm_lt_iff div_le_iff₀' one_div inv_pow inv_div Fintype.card.eq_1 Finset.prod_le_prod IsOrderedRing.toPosMulMono Real.instIsOrderedRing le_of_lt lt_trans Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one
mkContinuousLinear_norm_le 📖	mathematical	Real Real.instLE Real.instZero Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe MultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLikeForall LinearMap RingHom.id Semiring.toNonAssocSemiring addCommMonoid instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instFunLike Real.instMul Finset.prod Real.instCommMonoid Finset.univ	ContinuousLinearMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap ContinuousMultilinearMap.instTopologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup ContinuousMultilinearMap.instModule 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.hasOpNorm ContinuousMultilinearMap.seminormedAddCommGroup ContinuousMultilinearMap.normedSpace mkContinuousLinear	—	smulCommClass_self LE.le.trans_eq SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul mkContinuousLinear_norm_le' max_eq_left
mkContinuousLinear_norm_le' 📖	mathematical	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe MultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLikeForall LinearMap RingHom.id Semiring.toNonAssocSemiring addCommMonoid instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instFunLike Real.instMul Finset.prod Real.instCommMonoid Finset.univ	ContinuousLinearMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap ContinuousMultilinearMap.instTopologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup ContinuousMultilinearMap.instModule 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.hasOpNorm ContinuousMultilinearMap.seminormedAddCommGroup ContinuousMultilinearMap.normedSpace mkContinuousLinear Real.instMax Real.instZero	—	smulCommClass_self SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul LinearMap.mkContinuous_norm_le le_max_right
mkContinuousMultilinear_apply 📖	mathematical	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe MultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLikeForall addCommMonoid instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.instMul Finset.prod Real.instCommMonoid Finset.univ	ContinuousMultilinearMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap.funLike ContinuousMultilinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.instModule 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 ContinuousMultilinearMap.instTopologicalSpace mkContinuousMultilinear	—	smulCommClass_self IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
mkContinuousMultilinear_norm_le 📖	mathematical	Real Real.instLE Real.instZero Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe MultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLikeForall addCommMonoid instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.instMul Finset.prod Real.instCommMonoid Finset.univ	ContinuousMultilinearMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.instModule 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 ContinuousMultilinearMap.instTopologicalSpace ContinuousMultilinearMap.hasOpNorm ContinuousMultilinearMap.seminormedAddCommGroup ContinuousMultilinearMap.normedSpace mkContinuousMultilinear	—	smulCommClass_self LE.le.trans_eq IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul mkContinuousMultilinear_norm_le' max_eq_left
mkContinuousMultilinear_norm_le' 📖	mathematical	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe MultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLikeForall addCommMonoid instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.instMul Finset.prod Real.instCommMonoid Finset.univ	ContinuousMultilinearMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.instModule 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 ContinuousMultilinearMap.instTopologicalSpace ContinuousMultilinearMap.hasOpNorm ContinuousMultilinearMap.seminormedAddCommGroup ContinuousMultilinearMap.normedSpace mkContinuousMultilinear Real.instMax Real.instZero	—	smulCommClass_self IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul mkContinuous_norm_le le_max_right
mkContinuous_norm_le 📖	mathematical	Real Real.instLE Real.instZero Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe MultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLikeForall Real.instMul Finset.prod Real.instCommMonoid Finset.univ	ContinuousMultilinearMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap.hasOpNorm mkContinuous	—	ContinuousMultilinearMap.opNorm_le_bound
mkContinuous_norm_le' 📖	mathematical	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe MultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLikeForall Real.instMul Finset.prod Real.instCommMonoid Finset.univ	ContinuousMultilinearMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap.hasOpNorm mkContinuous Real.instMax Real.instZero	—	ContinuousMultilinearMap.opNorm_le_bound le_max_right LE.le.trans mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing le_max_left Finset.prod_nonneg Real.instZeroLEOneClass IsOrderedRing.toPosMulMono norm_nonneg
norm_image_sub_le_of_bound 📖	mathematical	Real Real.instLE Real.instZero Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe MultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLikeForall Real.instMul Finset.prod Real.instCommMonoid Finset.univ	SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Real.instNatCast Fintype.card Monoid.toNatPow Real.instMonoid Real.instMax Pi.seminormedAddCommGroup Pi.instSub	—	Finset.prod_le_prod Real.instZeroLEOneClass IsOrderedRing.toPosMulMono Real.instIsOrderedRing Mathlib.Meta.Positivity.ite_nonneg norm_nonneg le_max_of_le_left eq_or_ne Function.update_self norm_le_pi_norm Function.update_of_ne Finset.prod_update_of_mem Finset.mem_univ Finset.prod_const Finset.card_univ_diff Finset.card_singleton norm_image_sub_le_of_bound' mul_le_mul_of_nonneg_left Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Finset.sum_const Finset.card_univ nsmul_eq_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul
norm_image_sub_le_of_bound' 📖	mathematical	Real Real.instLE Real.instZero Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe MultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLikeForall Real.instMul Finset.prod Real.instCommMonoid Finset.univ	SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Finset.sum Real.instAddCommMonoid Real.instMax	—	Finset.induction Finset.piecewise_empty sub_self norm_zero MulZeroClass.mul_zero Finset.piecewise_insert Finset.piecewise_eq_of_notMem map_update_sub le_trans mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing Finset.prod_le_prod Real.instZeroLEOneClass norm_nonneg Function.update_self Function.update_of_ne Finset.piecewise_eq_of_mem dist_eq_norm dist_triangle add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add add_comm Finset.sum_insert left_distrib Distrib.leftDistribClass Finset.piecewise_univ
norm_map_coord_zero 📖	—	Continuous Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe MultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLikeForall Norm.norm SeminormedAddCommGroup.toNorm Real Real.instZero	—	—	inseparable_zero_iff_norm inseparable_pi Function.forall_update_iff Inseparable.symm map_update_zero Inseparable.map
restr_norm_le 📖	mathematical	Finset.card Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe MultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLikeForall Real.instMul Finset.prod Real.instCommMonoid Finset.univ Fin.fintype	restr Monoid.toNatPow Real.instMonoid	—	mul_right_comm mul_assoc Function.Bijective.prod_comp OrderIso.bijective Finset.prod_congr Fintype.prod_dite Finset.prod_const Fintype.card_of_subtype Finset.mem_compl Finset.card_compl Fintype.card_fin Lean.Meta.FastSubsingleton.elim Fintype.instFastSubsingleton

---

← Back to Index