Basic

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

Statistics

Metric	Count
Definitions mkContinuous, mkContinuousAlternating, mkContinuousLinear, compContinuousLinearMapCLM, constOfIsEmptyLIE, fderivCompContinuousLinearMap, fderivCompContinuousLinearMapCLM, instNormedAddCommGroup, instNormedSpace, instSeminormedAddCommGroup, ofSubsingletonLIE, piLIE, prodLIE, restrictScalarsLI, toContinuousMultilinearMapLI, continuousAlternatingMapCongr, continuousAlternatingMapCongrLeft, continuousAlternatingMapCongrRight, compContinuousAlternatingMapCLM, flipAlternating	20
Theorems 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, mkContinuousAlternating_apply, mkContinuousAlternating_norm_le, mkContinuousAlternating_norm_le_max, mkContinuousLinear_norm_le, mkContinuousLinear_norm_le_max, mkContinuous_norm_le, mkContinuous_norm_le', norm_image_sub_le_of_bound, norm_image_sub_le_of_bound', norm_map_coord_zero, bounds_bddBelow, bounds_nonempty, compContinuousLinearMapCLM_apply, constOfIsEmptyLIE_apply, constOfIsEmptyLIE_symm_apply, enorm_toContinuousMultilinearMap, fderivCompContinuousLinearMapCLM_apply, fderivCompContinuousLinearMap_apply, fderivCompContinuousLinearMap_of_isEmpty, instContinuousEval, isLeast_opNNNorm, isLeast_opNorm, 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_toContinuousMultilinearMap, norm_compContinuousLinearMap_le, norm_constOfIsEmpty, norm_def, norm_image_sub_le, norm_image_sub_le', norm_ofSubsingleton, norm_ofSubsingleton_id, norm_ofSubsingleton_id_le, norm_restrictScalars, norm_toContinuousMultilinearMap, ofSubsingletonLIE_apply, ofSubsingletonLIE_symm_apply, opNNNorm_le_iff, opNNNorm_pi, opNNNorm_prod, opNorm_le_bound, opNorm_le_iff, opNorm_pi, opNorm_prod, piLIE_apply_apply, piLIE_symm_apply_apply, prodLIE_apply, prodLIE_symm_apply, ratio_le_opNorm, restrictScalarsLI_apply, toContinuousMultilinearMapCLM_comp_fderivCompContinuousLinearMap, toContinuousMultilinearMapLI_apply, unit_le_opNorm, continuousAlternatingMapCongrLeft_apply, continuousAlternatingMapCongrRight_apply, continuousAlternatingMapCongrRight_symm, continuousAlternatingMapCongr_apply, compContinuousAlternatingMapCLM_apply_apply, flipAlternating_apply_apply, norm_compContinuousAlternatingMap_le, norm_compContinuousAlternatingMap	77
Total	97

AlternatingMap

Definitions

Name	Category	Theorems
mkContinuous 📖	CompOp	3 math math: coe_mkContinuous, mkContinuous_norm_le, mkContinuous_norm_le'
mkContinuousAlternating 📖	CompOp	3 math math: mkContinuousAlternating_norm_le, mkContinuousAlternating_norm_le_max, mkContinuousAlternating_apply
mkContinuousLinear 📖	CompOp	2 math math: mkContinuousLinear_norm_le, mkContinuousLinear_norm_le_max

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 AlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup instFunLike Real.instMul Finset.prod Real.instCommMonoid Finset.univ NormedAddCommGroup.toNorm	—	—	MultilinearMap.bound_of_shell
bound_of_shell_of_continuous 📖	—	Continuous Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe AlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLike Real Real.instLT Real.instZero Real.instOne Norm.norm NormedField.toNorm Real.instLE SeminormedAddCommGroup.toNorm Real.instMul Finset.prod Real.instCommMonoid Finset.univ	—	—	MultilinearMap.bound_of_shell_of_continuous
bound_of_shell_of_norm_map_coord_zero 📖	—	Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe AlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLike Real Real.instZero Real.instLT Real.instOne NormedField.toNorm Real.instLE Real.instMul Finset.prod Real.instCommMonoid Finset.univ	—	—	MultilinearMap.bound_of_shell_of_norm_map_coord_zero
coe_mkContinuous 📖	mathematical	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe AlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLike Real.instMul Finset.prod Real.instCommMonoid Finset.univ	ContinuousAlternatingMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousAlternatingMap.funLike mkContinuous	—	—
continuous_of_bound 📖	mathematical	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe AlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLike Real.instMul Finset.prod Real.instCommMonoid Finset.univ	Continuous Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	MultilinearMap.continuous_of_bound
exists_bound_of_continuous 📖	mathematical	Continuous Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe AlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLike	Real Real.instLT Real.instZero Real.instLE Norm.norm SeminormedAddCommGroup.toNorm Real.instMul Finset.prod Real.instCommMonoid Finset.univ	—	MultilinearMap.exists_bound_of_continuous
mkContinuousAlternating_apply 📖	mathematical	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe AlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLike instAddCommMonoid 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	ContinuousAlternatingMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousAlternatingMap.funLike ContinuousAlternatingMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousAlternatingMap.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 ContinuousAlternatingMap.instTopologicalSpace mkContinuousAlternating	—	smulCommClass_self IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
mkContinuousAlternating_norm_le 📖	mathematical	Real Real.instLE Real.instZero Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe AlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLike instAddCommMonoid 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	ContinuousAlternatingMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousAlternatingMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousAlternatingMap.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 ContinuousAlternatingMap.instTopologicalSpace ContinuousAlternatingMap.instSeminormedAddCommGroup ContinuousAlternatingMap.instNormedSpace mkContinuousAlternating	—	smulCommClass_self LE.le.trans_eq IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul mkContinuousAlternating_norm_le_max max_eq_left
mkContinuousAlternating_norm_le_max 📖	mathematical	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe AlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLike instAddCommMonoid 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	ContinuousAlternatingMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousAlternatingMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousAlternatingMap.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 ContinuousAlternatingMap.instTopologicalSpace ContinuousAlternatingMap.instSeminormedAddCommGroup ContinuousAlternatingMap.instNormedSpace mkContinuousAlternating Real.instMax Real.instZero	—	smulCommClass_self IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul mkContinuous_norm_le le_max_right
mkContinuousLinear_norm_le 📖	mathematical	Real Real.instLE Real.instZero Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe AlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLike LinearMap RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid 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 ContinuousAlternatingMap ContinuousAlternatingMap.instTopologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousAlternatingMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup ContinuousAlternatingMap.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 ContinuousAlternatingMap.instSeminormedAddCommGroup ContinuousAlternatingMap.instNormedSpace mkContinuousLinear	—	smulCommClass_self LE.le.trans_eq SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul mkContinuousLinear_norm_le_max max_eq_left
mkContinuousLinear_norm_le_max 📖	mathematical	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe AlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLike LinearMap RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid 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 ContinuousAlternatingMap ContinuousAlternatingMap.instTopologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousAlternatingMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup ContinuousAlternatingMap.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 ContinuousAlternatingMap.instSeminormedAddCommGroup ContinuousAlternatingMap.instNormedSpace mkContinuousLinear Real.instMax Real.instZero	—	smulCommClass_self LinearMap.mkContinuous_norm_le le_max_right
mkContinuous_norm_le 📖	mathematical	Real Real.instLE Real.instZero Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe AlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLike Real.instMul Finset.prod Real.instCommMonoid Finset.univ	ContinuousAlternatingMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousAlternatingMap.instSeminormedAddCommGroup mkContinuous	—	MultilinearMap.mkContinuous_norm_le
mkContinuous_norm_le' 📖	mathematical	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe AlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLike Real.instMul Finset.prod Real.instCommMonoid Finset.univ	ContinuousAlternatingMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousAlternatingMap.instSeminormedAddCommGroup 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 AlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLike 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	—	MultilinearMap.norm_image_sub_le_of_bound
norm_image_sub_le_of_bound' 📖	mathematical	Real Real.instLE Real.instZero Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe AlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLike Real.instMul Finset.prod Real.instCommMonoid Finset.univ	SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup Finset.sum Real.instAddCommMonoid Real.instMax	—	MultilinearMap.norm_image_sub_le_of_bound'
norm_map_coord_zero 📖	—	Continuous Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe AlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLike Norm.norm SeminormedAddCommGroup.toNorm Real Real.instZero	—	—	MultilinearMap.norm_map_coord_zero

ContinuousAlternatingMap

Definitions

Name	Category	Theorems
compContinuousLinearMapCLM 📖	CompOp	8 math math: hasStrictFDerivAt_compContinuousLinearMap, fderiv_continuousAlternatingMapCompContinuousLinearMap, fderivWithin_continuousAlternatingMapCompContinuousLinearMap, HasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap, fderivCompContinuousLinearMap_eq_alternatizeUncurryFin, HasStrictFDerivAt.continuousAlternatingMapCompContinuousLinearMap, HasFDerivAt.continuousAlternatingMapCompContinuousLinearMap, compContinuousLinearMapCLM_apply
constOfIsEmptyLIE 📖	CompOp	3 math math: constOfIsEmptyLIE_apply, alternatizeUncurryFin_constOfIsEmptyLIE_comp, constOfIsEmptyLIE_symm_apply
fderivCompContinuousLinearMap 📖	CompOp	12 math math: hasStrictFDerivAt_compContinuousLinearMap, fderiv_continuousAlternatingMapCompContinuousLinearMap, fderivWithin_continuousAlternatingMapCompContinuousLinearMap, HasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap, fderivCompContinuousLinearMap_eq_alternatizeUncurryFin, fderivCompContinuousLinearMapCLM_apply, toContinuousMultilinearMapCLM_comp_fderivCompContinuousLinearMap, fderivCompContinuousLinearMap_apply, fderivCompContinuousLinearMap_of_isEmpty, HasStrictFDerivAt.continuousAlternatingMapCompContinuousLinearMap, HasFDerivAt.continuousAlternatingMapCompContinuousLinearMap, alternatizeUncurryFin_fderivCompContinuousLinearMap_eq_zero
fderivCompContinuousLinearMapCLM 📖	CompOp	1 math math: fderivCompContinuousLinearMapCLM_apply
instNormedAddCommGroup 📖	CompOp	16 math math: hasStrictFDerivAt_compContinuousLinearMap, fderiv_continuousAlternatingMapCompContinuousLinearMap, alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_apply, norm_curryLeft, fderivWithin_continuousAlternatingMapCompContinuousLinearMap, norm_alternatizeUncurryFinCLM_le, HasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap, fderivCompContinuousLinearMap_eq_alternatizeUncurryFin, norm_ofSubsingleton_id, curryLeft_add, norm_alternatizeUncurryFin_le, alternatizeUncurryFin_add, alternatizeUncurryFin_curryLeft, HasStrictFDerivAt.continuousAlternatingMapCompContinuousLinearMap, HasFDerivAt.continuousAlternatingMapCompContinuousLinearMap, alternatizeUncurryFinCLM_apply
instNormedSpace 📖	CompOp	9 math math: norm_curryLeft, norm_alternatizeUncurryFinCLM_le, AlternatingMap.mkContinuousAlternating_norm_le, AlternatingMap.mkContinuousLinear_norm_le, curryLeftLI_apply, norm_alternatizeUncurryFin_le, AlternatingMap.mkContinuousAlternating_norm_le_max, ContinuousLinearMap.compContinuousAlternatingMapCLM_apply_apply, AlternatingMap.mkContinuousLinear_norm_le_max
instSeminormedAddCommGroup 📖	CompOp	56 math math: opNorm_prod, LinearIsometry.norm_compContinuousAlternatingMap, norm_constOfIsEmpty, norm_ofSubsingleton_id_le, opNNNorm_pi, piLIE_apply_apply, norm_def, le_opNNNorm, constOfIsEmptyLIE_apply, ofSubsingletonLIE_symm_apply, norm_restrictScalars, alternatizeUncurryFin_constOfIsEmptyLIE_comp, le_opNorm, norm_curryLeft, norm_alternatizeUncurryFinCLM_le, AlternatingMap.mkContinuousAlternating_norm_le, AlternatingMap.mkContinuous_norm_le, ofSubsingletonLIE_apply, toContinuousMultilinearMapLI_apply, norm_ofSubsingleton, constOfIsEmptyLIE_symm_apply, le_opNorm_mul_pow_of_le, norm_toContinuousMultilinearMap, isLeast_opNorm, fderivCompContinuousLinearMapCLM_apply, nnnorm_ofSubsingleton_id, restrictScalarsLI_apply, norm_image_sub_le', piLIE_symm_apply_apply, le_opNorm_mul_pow_card_of_le, ContinuousLinearMap.norm_compContinuousAlternatingMap_le, isLeast_opNNNorm, nnnorm_toContinuousMultilinearMap, opNorm_le_iff, prodLIE_apply, AlternatingMap.mkContinuousLinear_norm_le, curryLeftLI_apply, norm_alternatizeUncurryFin_le, opNorm_le_bound, AlternatingMap.mkContinuousAlternating_norm_le_max, nnnorm_ofSubsingleton, nnnorm_ofSubsingleton_id_le, nnnorm_constOfIsEmpty, ContinuousLinearMap.compContinuousAlternatingMapCLM_apply_apply, unit_le_opNorm, opNNNorm_le_iff, opNorm_pi, norm_compContinuousLinearMap_le, prodLIE_symm_apply, AlternatingMap.mkContinuousLinear_norm_le_max, opNNNorm_prod, enorm_toContinuousMultilinearMap, AlternatingMap.mkContinuous_norm_le', ratio_le_opNorm, norm_image_sub_le, le_opNorm_mul_prod_of_le
ofSubsingletonLIE 📖	CompOp	2 math math: ofSubsingletonLIE_symm_apply, ofSubsingletonLIE_apply
piLIE 📖	CompOp	2 math math: piLIE_apply_apply, piLIE_symm_apply_apply
prodLIE 📖	CompOp	2 math math: prodLIE_apply, prodLIE_symm_apply
restrictScalarsLI 📖	CompOp	1 math math: restrictScalarsLI_apply
toContinuousMultilinearMapLI 📖	CompOp	1 math math: toContinuousMultilinearMapLI_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bounds_bddBelow 📖	mathematical	—	BddBelow Real Real.instLE setOf Real.instZero	—	ContinuousMultilinearMap.bounds_bddBelow
bounds_nonempty 📖	mathematical	—	Real Set Set.instMembership setOf Real.instLE Real.instZero	—	ContinuousMultilinearMap.bounds_nonempty
compContinuousLinearMapCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ContinuousAlternatingMap 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 compContinuousLinearMapCLM compContinuousLinearMap	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self
constOfIsEmptyLIE_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousAlternatingMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instSeminormedAddCommGroup 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 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 LinearIsometryEquiv.instEquivLike constOfIsEmptyLIE constOfIsEmpty	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self
constOfIsEmptyLIE_symm_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousAlternatingMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instSeminormedAddCommGroup 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 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 LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm constOfIsEmptyLIE funLike Pi.instZero	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self
enorm_toContinuousMultilinearMap 📖	mathematical	—	ENorm.enorm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup ContinuousMultilinearMap.seminormedAddCommGroup' SeminormedAddGroup.toContinuousENorm toContinuousMultilinearMap ContinuousAlternatingMap instSeminormedAddCommGroup	—	—
fderivCompContinuousLinearMapCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ContinuousAlternatingMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instTopologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.topologicalSpace ContinuousLinearMap.addCommMonoid ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul instModule ContinuousLinearMap.addCommGroup NormedRing.toRing NormedCommRing.toNormedRing instAddCommGroup instIsTopologicalAddGroup instSeminormedAddCommGroup instSMulCommClass instContinuousConstSMul ContinuousLinearMap.funLike fderivCompContinuousLinearMapCLM fderivCompContinuousLinearMap	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul instIsTopologicalAddGroup instSMulCommClass instContinuousConstSMul
fderivCompContinuousLinearMap_apply 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap 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 ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup instTopologicalSpace addCommMonoid ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul instModule ContinuousLinearMap.funLike fderivCompContinuousLinearMap Finset.sum Finset.univ Function.update	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContinuousMultilinearMap.fderivCompContinuousLinearMap_apply Finset.sum_congr
fderivCompContinuousLinearMap_of_isEmpty 📖	mathematical	—	fderivCompContinuousLinearMap Pi.instZero ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup instTopologicalSpace addCommMonoid ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul instModule ContinuousLinearMap.zero	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.ext ext fderivCompContinuousLinearMap_apply Finset.sum_congr Finset.univ_eq_empty
instContinuousEval 📖	mathematical	—	ContinuousEval ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace funLike instTopologicalSpace Pi.topologicalSpace	—	ContinuousEval.of_continuous_forget ContinuousMultilinearMap.instContinuousEval continuous_toContinuousMultilinearMap
isLeast_opNNNorm 📖	mathematical	—	IsLeast NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal setOf NNNorm.nnnorm ContinuousAlternatingMap 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 instSeminormedAddCommGroup	—	ContinuousMultilinearMap.isLeast_opNNNorm
isLeast_opNorm 📖	mathematical	—	IsLeast Real Real.instLE setOf Real.instZero Norm.norm ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNorm instSeminormedAddCommGroup	—	ContinuousMultilinearMap.isLeast_opNorm
le_mul_prod_of_opNorm_le_of_le 📖	mathematical	Real Real.instLE Norm.norm ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNorm instSeminormedAddCommGroup	DFunLike.coe funLike Real.instMul Finset.prod Real.instCommMonoid Finset.univ	—	ContinuousMultilinearMap.le_mul_prod_of_opNorm_le_of_le
le_of_opNNNorm_le 📖	mathematical	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm ContinuousAlternatingMap 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 instSeminormedAddCommGroup	DFunLike.coe funLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Finset.prod CommSemiring.toCommMonoid instCommSemiringNNReal Finset.univ	—	ContinuousMultilinearMap.le_of_opNNNorm_le
le_of_opNorm_le 📖	mathematical	Real Real.instLE Norm.norm ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNorm instSeminormedAddCommGroup	DFunLike.coe funLike Real.instMul Finset.prod Real.instCommMonoid Finset.univ	—	ContinuousMultilinearMap.le_of_opNorm_le
le_opNNNorm 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe ContinuousAlternatingMap 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 instSeminormedAddCommGroup Finset.prod CommSemiring.toCommMonoid instCommSemiringNNReal Finset.univ	—	ContinuousMultilinearMap.le_opNNNorm
le_opNorm 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe ContinuousAlternatingMap 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 instSeminormedAddCommGroup Finset.prod Real.instCommMonoid Finset.univ	—	ContinuousMultilinearMap.le_opNorm
le_opNorm_mul_pow_card_of_le 📖	mathematical	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm Pi.seminormedAddCommGroup	DFunLike.coe ContinuousAlternatingMap 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 instSeminormedAddCommGroup Monoid.toNatPow Real.instMonoid Fintype.card	—	ContinuousMultilinearMap.le_opNorm_mul_pow_card_of_le
le_opNorm_mul_pow_of_le 📖	mathematical	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm Pi.seminormedAddCommGroup Fin.fintype	DFunLike.coe ContinuousAlternatingMap 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 instSeminormedAddCommGroup Monoid.toNatPow Real.instMonoid	—	ContinuousMultilinearMap.le_opNorm_mul_pow_of_le
le_opNorm_mul_prod_of_le 📖	mathematical	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm	DFunLike.coe ContinuousAlternatingMap 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 instSeminormedAddCommGroup Finset.prod Real.instCommMonoid Finset.univ	—	ContinuousMultilinearMap.le_opNorm_mul_prod_of_le
nnnorm_constOfIsEmpty 📖	mathematical	—	NNNorm.nnnorm ContinuousAlternatingMap 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 instSeminormedAddCommGroup constOfIsEmpty	—	NNReal.eq norm_constOfIsEmpty
nnnorm_ofSubsingleton 📖	mathematical	—	NNNorm.nnnorm ContinuousAlternatingMap 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 instSeminormedAddCommGroup 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 ContinuousAlternatingMap 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 instSeminormedAddCommGroup 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 ContinuousAlternatingMap 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 instSeminormedAddCommGroup DFunLike.coe Equiv ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike ofSubsingleton ContinuousLinearMap.id instOneNNReal	—	ContinuousMultilinearMap.nnnorm_ofSubsingleton_id_le
nnnorm_toContinuousMultilinearMap 📖	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 ContinuousMultilinearMap.seminormedAddCommGroup' toContinuousMultilinearMap ContinuousAlternatingMap instSeminormedAddCommGroup	—	—
norm_compContinuousLinearMap_le 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNorm instSeminormedAddCommGroup compContinuousLinearMap Real.instMul Monoid.toNatPow Real.instMonoid ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.hasOpNorm Fintype.card	—	LE.le.trans_eq ContinuousMultilinearMap.norm_compContinuousLinearMap_le Finset.prod_const
norm_constOfIsEmpty 📖	mathematical	—	Norm.norm ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNorm instSeminormedAddCommGroup constOfIsEmpty	—	ContinuousMultilinearMap.norm_constOfIsEmpty
norm_def 📖	mathematical	—	Norm.norm ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNorm instSeminormedAddCommGroup 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 ContinuousAlternatingMap 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 instSeminormedAddCommGroup Real.instNatCast Fintype.card Monoid.toNatPow Real.instMonoid Real.instMax Pi.seminormedAddCommGroup Pi.instSub	—	ContinuousMultilinearMap.norm_image_sub_le
norm_image_sub_le' 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe ContinuousAlternatingMap 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 instSeminormedAddCommGroup Finset.sum Real.instAddCommMonoid Finset.univ Finset.prod Real.instCommMonoid Real.instMax	—	ContinuousMultilinearMap.norm_image_sub_le'
norm_ofSubsingleton 📖	mathematical	—	Norm.norm ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNorm instSeminormedAddCommGroup DFunLike.coe Equiv ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike ofSubsingleton ContinuousLinearMap.hasOpNorm	—	ContinuousMultilinearMap.norm_ofSubsingleton
norm_ofSubsingleton_id 📖	mathematical	—	Norm.norm ContinuousAlternatingMap 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 NormedAddCommGroup.toNorm instNormedAddCommGroup DFunLike.coe Equiv ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike ofSubsingleton ContinuousLinearMap.id Real Real.instOne	—	ContinuousMultilinearMap.norm_ofSubsingleton_id
norm_ofSubsingleton_id_le 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNorm instSeminormedAddCommGroup DFunLike.coe Equiv ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring EquivLike.toFunLike Equiv.instEquivLike ofSubsingleton ContinuousLinearMap.id Real.instOne	—	ContinuousMultilinearMap.norm_ofSubsingleton_id_le
norm_restrictScalars 📖	mathematical	—	Norm.norm ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNorm instSeminormedAddCommGroup restrictScalars Algebra.toSMul Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedAlgebra.toAlgebra	—	—
norm_toContinuousMultilinearMap 📖	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' toContinuousMultilinearMap ContinuousAlternatingMap SeminormedAddCommGroup.toNorm instSeminormedAddCommGroup	—	—
ofSubsingletonLIE_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 ContinuousAlternatingMap ContinuousLinearMap.toSeminormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instSeminormedAddCommGroup 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 ofSubsingletonLIE Equiv Equiv.instEquivLike ofSubsingleton	—	RingHomInvPair.ids RingHomIsometric.ids smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup
ofSubsingletonLIE_symm_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousAlternatingMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousLinearMap instSeminormedAddCommGroup 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 ofSubsingletonLIE Equiv Equiv.instEquivLike Equiv.symm 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 ContinuousAlternatingMap 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 instSeminormedAddCommGroup DFunLike.coe funLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Finset.prod CommSemiring.toCommMonoid instCommSemiringNNReal Finset.univ	—	ContinuousMultilinearMap.opNNNorm_le_iff
opNNNorm_pi 📖	mathematical	—	NNNorm.nnnorm ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Pi.addCommMonoid Pi.module Pi.topologicalSpace SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup instSeminormedAddCommGroup Pi.seminormedAddCommGroup Pi.normedSpace pi Pi.seminormedAddGroup	—	ContinuousMultilinearMap.opNNNorm_pi
opNNNorm_prod 📖	mathematical	—	NNNorm.nnnorm ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Prod.instAddCommMonoid Prod.instModule instTopologicalSpaceProd SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup instSeminormedAddCommGroup Prod.seminormedAddCommGroup Prod.normedSpace prod NNReal NNReal.instMax	—	ContinuousMultilinearMap.opNNNorm_prod
opNorm_le_bound 📖	mathematical	Real Real.instLE Real.instZero Norm.norm SeminormedAddCommGroup.toNorm DFunLike.coe ContinuousAlternatingMap 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	instSeminormedAddCommGroup	—	ContinuousMultilinearMap.opNorm_le_bound
opNorm_le_iff 📖	mathematical	Real Real.instLE Real.instZero	Norm.norm ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNorm instSeminormedAddCommGroup DFunLike.coe funLike Real.instMul Finset.prod Real.instCommMonoid Finset.univ	—	ContinuousMultilinearMap.opNorm_le_iff
opNorm_pi 📖	mathematical	—	Norm.norm ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Pi.addCommMonoid Pi.module Pi.topologicalSpace SeminormedAddCommGroup.toNorm instSeminormedAddCommGroup Pi.seminormedAddCommGroup Pi.normedSpace pi	—	ContinuousMultilinearMap.opNorm_pi
opNorm_prod 📖	mathematical	—	Norm.norm ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Prod.instAddCommMonoid Prod.instModule instTopologicalSpaceProd SeminormedAddCommGroup.toNorm instSeminormedAddCommGroup Prod.seminormedAddCommGroup Prod.normedSpace prod Real Real.instMax	—	ContinuousMultilinearMap.opNorm_prod
piLIE_apply_apply 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Pi.addCommMonoid Pi.module Pi.topologicalSpace funLike LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.seminormedAddCommGroup instSeminormedAddCommGroup Pi.normedSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup instModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid 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 piLIE	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self instContinuousConstSMulForall Pi.smulCommClass
piLIE_symm_apply_apply 📖	mathematical	—	DFunLike.coe ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace funLike LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid Pi.module Pi.topologicalSpace instSeminormedAddCommGroup 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 DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup 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 EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm piLIE	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup instContinuousConstSMulForall UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Pi.smulCommClass smulCommClass_self IsTopologicalAddGroup.toContinuousAdd
prodLIE_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousAlternatingMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Prod.instAddCommMonoid Prod.instModule instTopologicalSpaceProd Prod.seminormedAddCommGroup instSeminormedAddCommGroup 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 prodLIE prod	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self Prod.continuousConstSMul Prod.smulCommClass
prodLIE_symm_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousAlternatingMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Prod.instAddCommMonoid Prod.instModule instTopologicalSpaceProd instSeminormedAddCommGroup 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 prodLIE ContinuousLinearMap.compContinuousAlternatingMap ContinuousLinearMap.fst ContinuousLinearMap.snd	—	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 ContinuousAlternatingMap 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 instSeminormedAddCommGroup	—	ContinuousMultilinearMap.ratio_le_opNorm
restrictScalarsLI_apply 📖	mathematical	—	DFunLike.coe LinearIsometry DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ContinuousAlternatingMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instSeminormedAddCommGroup 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 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 IsScalarTower.to_smulCommClass' Semifield.toCommSemiring NormedAlgebra.toAlgebra smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing LinearIsometry.instFunLike restrictScalarsLI restrictScalars Algebra.toSMul SeminormedRing.toRing	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsScalarTower.to_smulCommClass' smulCommClass_self
toContinuousMultilinearMapCLM_comp_fderivCompContinuousLinearMap 📖	mathematical	—	ContinuousLinearMap.comp DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup ContinuousAlternatingMap instTopologicalSpace addCommMonoid AddCommGroup.toAddGroup ContinuousMultilinearMap ContinuousMultilinearMap.instTopologicalSpace ContinuousMultilinearMap.addCommMonoid ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul instModule ContinuousMultilinearMap.instModule RingHomCompTriple.ids toContinuousMultilinearMapCLM fderivCompContinuousLinearMap Pi.topologicalSpace Pi.addCommMonoid Pi.module SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid ContinuousMultilinearMap.fderivCompContinuousLinearMap toContinuousMultilinearMap ContinuousLinearMap.pi ContinuousLinearMap.id	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomCompTriple.ids
toContinuousMultilinearMapLI_apply 📖	mathematical	—	DFunLike.coe LinearIsometry DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ContinuousAlternatingMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap instSeminormedAddCommGroup ContinuousMultilinearMap.seminormedAddCommGroup' 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 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 ContinuousMultilinearMap.instModule LinearIsometry.instFunLike toContinuousMultilinearMapLI toContinuousMultilinearMap	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self
unit_le_opNorm 📖	mathematical	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm Pi.seminormedAddCommGroup Real.instOne	DFunLike.coe ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace funLike instSeminormedAddCommGroup	—	ContinuousMultilinearMap.unit_le_opNorm

ContinuousLinearEquiv

Definitions

Name	Category	Theorems
continuousAlternatingMapCongr 📖	CompOp	1 math math: continuousAlternatingMapCongr_apply
continuousAlternatingMapCongrLeft 📖	CompOp	1 math math: continuousAlternatingMapCongrLeft_apply
continuousAlternatingMapCongrRight 📖	CompOp	2 math math: continuousAlternatingMapCongrRight_symm, continuousAlternatingMapCongrRight_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousAlternatingMapCongrLeft_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousAlternatingMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousAlternatingMap.instTopologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousAlternatingMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup ContinuousAlternatingMap.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 continuousAlternatingMapCongrLeft ContinuousAlternatingMap.compContinuousLinearMap toContinuousLinearMap symm	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self
continuousAlternatingMapCongrRight_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousAlternatingMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousAlternatingMap.instTopologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousAlternatingMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup ContinuousAlternatingMap.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 continuousAlternatingMapCongrRight ContinuousLinearMap.compContinuousAlternatingMap toContinuousLinearMap	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self
continuousAlternatingMapCongrRight_symm 📖	mathematical	—	symm DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousAlternatingMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousAlternatingMap.instTopologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousAlternatingMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup ContinuousAlternatingMap.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 continuousAlternatingMapCongrRight	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self
continuousAlternatingMapCongr_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousAlternatingMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousAlternatingMap.instTopologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousAlternatingMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup ESeminormedAddCommMonoid.toAddCommMonoid NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousAlternatingMap.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 NormedAddCommGroup.toAddCommGroup EquivLike.toFunLike equivLike continuousAlternatingMapCongr ContinuousLinearMap.compContinuousAlternatingMap toContinuousLinearMap ContinuousAlternatingMap.compContinuousLinearMap symm	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self

ContinuousLinearMap

Definitions

Name	Category	Theorems
compContinuousAlternatingMapCLM 📖	CompOp	1 math math: compContinuousAlternatingMapCLM_apply_apply
flipAlternating 📖	CompOp	6 math math: fderiv_continuousAlternatingMap_apply_const, HasFDerivAt.continuousAlternatingMap_apply_const, fderivWithin_continuousAlternatingMap_apply_const, HasStrictFDerivAt.continuousAlternatingMap_apply_const, HasFDerivWithinAt.continuousAlternatingMap_apply_const, flipAlternating_apply_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compContinuousAlternatingMapCLM_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 ContinuousAlternatingMap AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousAlternatingMap.instSeminormedAddCommGroup ContinuousAlternatingMap.instNormedSpace funLike topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup ContinuousAlternatingMap.instTopologicalSpace ContinuousAlternatingMap.addCommMonoid ContinuousAlternatingMap.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 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 CommRing.toRing ContinuousAlternatingMap.instAddCommGroup ContinuousAlternatingMap.instIsTopologicalAddGroup module ContinuousAlternatingMap.instSMulCommClass ContinuousAlternatingMap.instContinuousConstSMul compContinuousAlternatingMapCLM compContinuousAlternatingMap CommSemiring.toSemiring Semifield.toCommSemiring	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self ContinuousAlternatingMap.instIsTopologicalAddGroup ContinuousAlternatingMap.instSMulCommClass ContinuousAlternatingMap.instContinuousConstSMul
flipAlternating_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 ContinuousAlternatingMap 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 ContinuousAlternatingMap.funLike flipAlternating ContinuousAlternatingMap.instTopologicalSpace ContinuousAlternatingMap.addCommMonoid ContinuousAlternatingMap.instModule	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self
norm_compContinuousAlternatingMap_le 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousAlternatingMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNorm ContinuousAlternatingMap.instSeminormedAddCommGroup compContinuousAlternatingMap Real.instMul ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring hasOpNorm	—	norm_compContinuousMultilinearMap_le

LinearIsometry

Theorems

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

---

← Back to Index