Composition

📁 Source: Mathlib/Analysis/Analytic/Composition.lean

Statistics

Metric	Count
Definitions gather, sigmaCompositionAux, sigmaEquivSigmaPi, compAlongComposition, applyComposition, comp, compAlongComposition, compChangeOfVariables, compPartialSumSource, compPartialSumTarget, compPartialSumTargetSet, id	12
Theorems comp, comp', comp_analyticWithinAt, comp_analyticWithinAt_of_eq, comp_of_eq, comp_of_eq', comp, comp, comp', comp_analyticOn, comp, comp_of_eq, comp, comp_of_eq, fun_comp, fun_comp_of_eq, comp, comp', blocksFun_sigmaCompositionAux, length_gather, length_sigmaCompositionAux, sigma_composition_eq_iff, sigma_pi_composition_eq_iff, sizeUpTo_sizeUpTo_add, compAlongComposition_apply, applyComposition_ones, applyComposition_single, applyComposition_update, compAlongComposition_apply, compAlongComposition_bound, compAlongComposition_nnnorm, compAlongComposition_norm, compChangeOfVariables_blocksFun, compChangeOfVariables_length, compChangeOfVariables_sum, compContinuousLinearMap_applyComposition, compPartialSumTargetSet_image_compPartialSumSource, compPartialSumTarget_tendsto_atTop, compPartialSumTarget_tendsto_prod_atTop, comp_assoc, comp_coeff_one, comp_coeff_zero, comp_coeff_zero', comp_coeff_zero'', comp_id, comp_partialSum, comp_removeZero, comp_summable_nnreal, id_apply_of_one_lt, id_apply_one, id_apply_one', id_apply_zero, id_comp, id_comp', le_comp_radius_of_summable, mem_compPartialSumSource_iff, mem_compPartialSumTarget_iff, removeZero_applyComposition, removeZero_comp_of_pos, comp, comp, comp	62
Total	74

AnalyticAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	AnalyticAt	AnalyticAt	—	analyticWithinAt_univ AnalyticWithinAt.comp
comp' 📖	mathematical	AnalyticAt	AnalyticAt	—	comp
comp_analyticWithinAt 📖	mathematical	AnalyticAt AnalyticWithinAt	AnalyticWithinAt	—	AnalyticWithinAt.comp analyticWithinAt_univ Set.mapsTo_univ
comp_analyticWithinAt_of_eq 📖	mathematical	AnalyticAt AnalyticWithinAt	AnalyticWithinAt	—	comp_analyticWithinAt
comp_of_eq 📖	mathematical	AnalyticAt	AnalyticAt	—	comp
comp_of_eq' 📖	mathematical	AnalyticAt	AnalyticAt	—	comp_of_eq

AnalyticOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	AnalyticOn Set.MapsTo	AnalyticOn	—	AnalyticWithinAt.comp

AnalyticOnNhd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	AnalyticOnNhd Set.MapsTo	AnalyticOnNhd	—	comp' mono Set.mapsTo_iff_image_subset
comp' 📖	mathematical	AnalyticOnNhd Set.image	AnalyticOnNhd	—	AnalyticAt.comp Set.mem_image_of_mem
comp_analyticOn 📖	mathematical	AnalyticOnNhd AnalyticOn Set.MapsTo	AnalyticOn	—	AnalyticAt.comp_analyticWithinAt

AnalyticWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	AnalyticWithinAt Set.MapsTo	AnalyticWithinAt	—	HasFPowerSeriesWithinAt.analyticWithinAt SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul HasFPowerSeriesWithinAt.comp
comp_of_eq 📖	mathematical	AnalyticWithinAt Set.MapsTo	AnalyticWithinAt	—	comp

CPolynomialAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	CPolynomialAt	CPolynomialAt	—	SeminormedAddCommGroup.toIsTopologicalAddGroup HasFiniteFPowerSeriesAt.comp HasFiniteFPowerSeriesAt.of_le
comp_of_eq 📖	mathematical	CPolynomialAt	CPolynomialAt	—	comp
fun_comp 📖	mathematical	CPolynomialAt	CPolynomialAt	—	comp
fun_comp_of_eq 📖	mathematical	CPolynomialAt	CPolynomialAt	—	comp_of_eq

CPolynomialOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	CPolynomialOn Set.MapsTo	CPolynomialOn	—	comp' mono Set.mapsTo_iff_image_subset
comp' 📖	mathematical	CPolynomialOn Set.image	CPolynomialOn	—	CPolynomialAt.comp Set.mem_image_of_mem

Composition

Definitions

Name	Category	Theorems
gather 📖	CompOp	4 math math: blocksFun_sigmaCompositionAux, length_sigmaCompositionAux, length_gather, sizeUpTo_sizeUpTo_add
sigmaCompositionAux 📖	CompOp	3 math math: blocksFun_sigmaCompositionAux, length_sigmaCompositionAux, sizeUpTo_sizeUpTo_add
sigmaEquivSigmaPi 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
blocksFun_sigmaCompositionAux 📖	mathematical	—	blocksFun gather length length_gather sigmaCompositionAux length_sigmaCompositionAux DFunLike.coe OrderEmbedding instFunLikeOrderEmbedding embedding	—	length_gather length_sigmaCompositionAux blocksFun.eq_1 List.getElem_splitWrtComposition
length_gather 📖	mathematical	—	length gather	—	List.length_splitWrtComposition
length_sigmaCompositionAux 📖	mathematical	—	length blocksFun gather length_gather sigmaCompositionAux	—	List.length_splitWrtComposition instReflLe List.getElem_map_rev List.map_length_splitWrtComposition blocksFun.eq_1
sigma_composition_eq_iff 📖	mathematical	—	blocks Composition length	—	ext
sigma_pi_composition_eq_iff 📖	mathematical	—	length Composition blocks blocksFun	—	ext blocks_sum ofFn_blocksFun
sizeUpTo_sizeUpTo_add 📖	mathematical	length blocksFun	sizeUpTo length gather blocksFun length_gather sigmaCompositionAux	—	length_gather List.length_splitWrtComposition blocks_pos' List.sum_take_succ min_eq_left List.monotone_sum_take Nat.instCanonicallyOrderedAdd List.getElem_splitWrtComposition lt_trans lt_add_one Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid length_sigmaCompositionAux sizeUpTo_succ contravariant_lt_of_covariant_le lt_of_lt_of_le sizeUpTo_le add_assoc

ContinuousMultilinearMap

Definitions

Name	Category	Theorems
compAlongComposition 📖	CompOp	2 math math: FormalMultilinearSeries.compAlongComposition_bound, compAlongComposition_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compAlongComposition_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid funLike compAlongComposition Composition.length FormalMultilinearSeries.applyComposition	—	IsTopologicalAddGroup.toContinuousAdd

FormalMultilinearSeries

Definitions

Name	Category	Theorems
applyComposition 📖	CompOp	9 math math: comp_rightInv_aux1, applyComposition_single, compContinuousLinearMap_applyComposition, compAlongComposition_apply, ContinuousMultilinearMap.compAlongComposition_apply, applyComposition_update, comp_rightInv_aux2, removeZero_applyComposition, applyComposition_ones
comp 📖	CompOp	17 math math: comp_rightInv_aux1, HasFPowerSeriesAt.comp, comp_coeff_zero, comp_removeZero, id_comp', removeZero_comp_of_pos, comp_id, comp_coeff_one, id_comp, le_comp_radius_of_summable, comp_coeff_zero', comp_coeff_zero'', leftInv_comp, comp_rightInv, HasFiniteFPowerSeriesAt.comp, comp_assoc, HasFPowerSeriesWithinAt.comp
compAlongComposition 📖	CompOp	6 math math: comp_partialSum, compAlongComposition_nnnorm, compAlongComposition_norm, compAlongComposition_apply, rightInv_coeff, comp_summable_nnreal
compChangeOfVariables 📖	CompOp	3 math math: compPartialSumTargetSet_image_compPartialSumSource, compChangeOfVariables_blocksFun, compChangeOfVariables_length
compPartialSumSource 📖	CompOp	3 math math: compPartialSumTargetSet_image_compPartialSumSource, mem_compPartialSumSource_iff, compChangeOfVariables_sum
compPartialSumTarget 📖	CompOp	5 math math: comp_partialSum, compPartialSumTarget_tendsto_atTop, mem_compPartialSumTarget_iff, compPartialSumTarget_tendsto_prod_atTop, compChangeOfVariables_sum
compPartialSumTargetSet 📖	CompOp	—
id 📖	CompOp	9 math math: id_apply_one', id_comp', comp_id, id_comp, id_apply_zero, leftInv_comp, comp_rightInv, id_apply_of_one_lt, id_apply_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
applyComposition_ones 📖	mathematical	—	applyComposition Composition.ones DFunLike.coe ContinuousMultilinearMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ContinuousMultilinearMap.funLike Composition.length Composition.length_le	—	IsTopologicalAddGroup.toContinuousAdd Composition.length_le congr Composition.ones_blocksFun lt_of_lt_of_le Composition.ones_embedding
applyComposition_single 📖	mathematical	—	applyComposition Composition.single DFunLike.coe ContinuousMultilinearMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ContinuousMultilinearMap.funLike	—	IsTopologicalAddGroup.toContinuousAdd congr Composition.single_blocksFun le_bot_iff Function.hfunext Composition.single_embedding
applyComposition_update 📖	mathematical	—	applyComposition Function.update Composition.length Composition.index DFunLike.coe ContinuousMultilinearMap Composition.blocksFun CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ContinuousMultilinearMap.funLike OrderEmbedding instFunLikeOrderEmbedding Composition.embedding Composition.invEmbedding	—	IsTopologicalAddGroup.toContinuousAdd Function.update_self Function.update_comp_eq_of_injective RelEmbedding.injective Composition.embedding_comp_inv Function.update_of_ne Function.update_comp_eq_of_notMem_range Composition.mem_range_embedding_iff'
compAlongComposition_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ContinuousMultilinearMap.funLike compAlongComposition Composition.length applyComposition	—	IsTopologicalAddGroup.toContinuousAdd
compAlongComposition_bound 📖	mathematical	—	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm DFunLike.coe ContinuousMultilinearMap CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap.funLike ContinuousMultilinearMap.compAlongComposition SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield 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 Real.instMul Composition.length ContinuousMultilinearMap.hasOpNorm' Fin.fintype Finset.prod Real.instCommMonoid Finset.univ Composition.blocksFun	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContinuousMultilinearMap.le_opNorm mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing Finset.prod_le_prod Real.instZeroLEOneClass norm_nonneg Finset.prod_mul_distrib mul_assoc Equiv.prod_comp Finset.univ_sigma_univ Finset.prod_sigma
compAlongComposition_nnnorm 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder NNNorm.nnnorm ContinuousMultilinearMap CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousMultilinearMap.seminormedAddCommGroup' Fin.fintype compAlongComposition SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield 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 Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring Composition.length Finset.prod CommSemiring.toCommMonoid NNReal.instCommSemiring Finset.univ Composition.blocksFun	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul NNReal.coe_le_coe NNReal.coe_prod Finset.prod_congr compAlongComposition_norm
compAlongComposition_norm 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousMultilinearMap CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousMultilinearMap.hasOpNorm' Fin.fintype compAlongComposition SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield 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 Real.instMul Composition.length Finset.prod Real.instCommMonoid Finset.univ Composition.blocksFun	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContinuousMultilinearMap.opNorm_le_bound mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing norm_nonneg Finset.prod_nonneg Real.instZeroLEOneClass compAlongComposition_bound
compChangeOfVariables_blocksFun 📖	mathematical	Finset SetLike.instMembership Finset.instSetLike compPartialSumSource	Composition.blocksFun Composition compChangeOfVariables Composition.length compChangeOfVariables_length	—	compChangeOfVariables_length
compChangeOfVariables_length 📖	mathematical	Finset SetLike.instMembership Finset.instSetLike compPartialSumSource	Composition.length Composition compChangeOfVariables	—	—
compChangeOfVariables_sum 📖	mathematical	compChangeOfVariables	Finset.sum compPartialSumSource Composition compPartialSumTarget	—	Finset.sum_bij mem_compPartialSumSource_iff List.get_ofFn compChangeOfVariables_length compChangeOfVariables_blocksFun compPartialSumTargetSet_image_compPartialSumSource
compContinuousLinearMap_applyComposition 📖	mathematical	—	applyComposition compContinuousLinearMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike	—	IsTopologicalAddGroup.toContinuousAdd
compPartialSumTargetSet_image_compPartialSumSource 📖	mathematical	Composition Set Set.instMembership compPartialSumTargetSet	Finset SetLike.instMembership Finset.instSetLike compPartialSumSource compChangeOfVariables	—	Composition.one_le_blocks' Composition.sigma_eq_iff_blocks_eq List.ofFn_get
compPartialSumTarget_tendsto_atTop 📖	mathematical	—	Filter.Tendsto Finset Composition compPartialSumTarget Filter.atTop Nat.instPreorder PartialOrder.toPreorder Finset.partialOrder	—	Filter.Tendsto.comp compPartialSumTarget_tendsto_prod_atTop Filter.tendsto_atTop_diagonal
compPartialSumTarget_tendsto_prod_atTop 📖	mathematical	—	Filter.Tendsto Finset Composition compPartialSumTarget Filter.atTop Prod.instPreorder Nat.instPreorder PartialOrder.toPreorder Finset.partialOrder	—	Monotone.tendsto_atTop_finset lt_of_lt_of_le Nat.instCanonicallyOrderedAdd Finset.bddAbove bot_le lt_of_le_of_lt le_max_right lt_add_one Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid le_trans le_max_left
comp_assoc 📖	mathematical	—	comp Field.toCommRing NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield 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	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ext ContinuousMultilinearMap.ext Equiv.sum_comp Finset.sum_congr congr Composition.length_gather Composition.length_sigmaCompositionAux Composition.blocksFun_sigmaCompositionAux Composition.sizeUpTo_sizeUpTo_add add_assoc ContinuousMultilinearMap.sum_apply Finset.sum_sigma' ContinuousMultilinearMap.map_sum
comp_coeff_one 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ContinuousMultilinearMap.funLike comp	—	IsTopologicalAddGroup.toContinuousAdd Finset.eq_univ_of_card Finset.card_singleton composition_card tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub pow_zero Finset.sum_congr Finset.sum_singleton congr Composition.ones_length Composition.length_le applyComposition_ones Lean.Meta.FastSubsingleton.elim Lean.Meta.instFastSubsingletonFinOfNatNat
comp_coeff_zero 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ContinuousMultilinearMap.funLike comp	—	IsTopologicalAddGroup.toContinuousAdd Finset.eq_of_subset_of_card_le composition_card zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub pow_zero Finset.card_singleton instReflLe Finset.sum_singleton compAlongComposition_apply Lean.Meta.FastSubsingleton.helim Lean.Meta.instFastSubsingletonForallOfFastIsEmpty Lean.Meta.instFastIsEmptyFinOfNatNat Function.hfunext
comp_coeff_zero' 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ContinuousMultilinearMap.funLike comp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	IsTopologicalAddGroup.toContinuousAdd comp_coeff_zero
comp_coeff_zero'' 📖	mathematical	—	comp	—	IsTopologicalAddGroup.toContinuousAdd ContinuousMultilinearMap.ext comp_coeff_zero
comp_id 📖	mathematical	—	comp Field.toCommRing NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield 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 id	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ext Finset.sum_eq_single Composition.ne_ones_iff Fin.prop Composition.blocks_length ContinuousMultilinearMap.ext compAlongComposition_apply ContinuousMultilinearMap.zero_apply ContinuousMultilinearMap.map_coord_zero id_apply_of_one_lt instIsEmptyFalse congr Composition.ones_length Composition.length_le applyComposition_ones
comp_partialSum 📖	mathematical	—	partialSum 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 IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup 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 NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul Finset.sum Finset.Ico Nat.instPreorder Nat.instLocallyFiniteOrder DFunLike.coe ContinuousMultilinearMap ContinuousMultilinearMap.funLike Composition compPartialSumTarget CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing AddCommGroup.toAddCommMonoid compAlongComposition	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Finset.range_eq_Ico Finset.sum_sigma' compChangeOfVariables_sum congr compChangeOfVariables_length compChangeOfVariables_blocksFun applyComposition.eq_1 Finset.sum_congr ContinuousMultilinearMap.map_sum_finset
comp_removeZero 📖	mathematical	—	comp removeZero CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup	—	IsTopologicalAddGroup.toContinuousAdd ext ContinuousMultilinearMap.ext ContinuousMultilinearMap.sum_apply Finset.sum_congr removeZero_applyComposition
comp_summable_nnreal 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal radius	NNReal Preorder.toLT PartialOrder.toPreorder NNReal.instPartialOrder NNReal.instZero Summable Composition NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring NNReal.instTopologicalSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NNNorm.nnnorm ContinuousMultilinearMap CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousMultilinearMap.seminormedAddCommGroup' Fin.fintype compAlongComposition SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield 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 Monoid.toPow SummationFilter.unconditional	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ENNReal.lt_iff_exists_nnreal_btwn lt_min zero_lt_one IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing NeZero.charZero_one ENNReal.instCharZero nnnorm_mul_pow_le_of_lt_radius le_max_right LE.le.trans le_max_left Nat.instAtLeastTwoHAddOfNat inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono mul_pos zero_lt_four LinearOrderedCommMonoidWithZero.toZeroLeOneClass IsStrictOrderedRing.toCharZero NNReal.addLeftMono LT.lt.trans_le mul_le_mul' NNReal.mulLeftMono covariant_swap_mul_of_covariant_mul le_rfl pow_le_pow_of_le_one IsOrderedRing.toPosMulMono Real.instIsOrderedRing LT.lt.le Composition.length_le Finset.prod_mul_distrib Finset.prod_pow_eq_pow_sum Composition.sum_blocksFun Finset.prod_le_prod' Finset.prod_const Fintype.card_fin pow_right_mono₀ le_imp_le_of_le_of_le mul_le_mul_left compAlongComposition_nnnorm le_refl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.one_pow mul_inv_rev mul_pow inv_pow Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero one_mul Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt pow_pos IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toZeroLEOneClass lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat Nat.cast_one Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial NNReal.summable_of_le div_eq_mul_inv Summable.mul_left NNReal.instIsTopologicalSemiring Finset.sum_const composition_card nsmul_eq_mul Nat.cast_pow hasSum_fintype SummationFilter.instLeAtTopUnconditional NNReal.summable_sigma HasSum.summable NNReal.summable_nat_add_iff HasSum.tsum_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_mul pow_succ one_div Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Meta.NormNum.isNat_eq_false Nat.cast_zero NNReal.summable_geometric NNReal.div_lt_one_of_lt one_lt_two IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono IsStrictOrderedRing.toIsOrderedCancelAddMonoid
id_apply_of_one_lt 📖	mathematical	—	id ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.instZero	—	—
id_apply_one 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.funLike id	—	—
id_apply_one' 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.funLike id zero_lt_one MulZeroClass.toZero Nat.instMulZeroClass Nat.instOne Nat.instPartialOrder Nat.instZeroLEOneClass	—	zero_lt_one Nat.instZeroLEOneClass id_apply_one
id_apply_zero 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.funLike id	—	—
id_comp 📖	mathematical	—	comp Field.toCommRing NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield 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 id DFunLike.coe ContinuousMultilinearMap ContinuousMultilinearMap.funLike	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ext ContinuousMultilinearMap.ext comp_coeff_zero' Finset.sum_eq_single Composition.length_pos_of_pos compAlongComposition_apply id_apply_of_one_lt ContinuousMultilinearMap.zero_apply instIsEmptyFalse zero_lt_one Nat.instZeroLEOneClass Composition.single_length id_apply_one' congr Composition.single_embedding
id_comp' 📖	mathematical	DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.funLike	comp Field.toCommRing NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield 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 id	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul id_comp
le_comp_radius_of_summable 📖	mathematical	Summable NNReal Composition NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring NNReal.instTopologicalSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NNNorm.nnnorm ContinuousMultilinearMap CommSemiring.toSemiring CommRing.toCommSemiring Field.toCommRing NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousMultilinearMap.seminormedAddCommGroup' Fin.fintype compAlongComposition SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield 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 Monoid.toPow SummationFilter.unconditional	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.ofNNReal radius comp Field.toCommRing NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield 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	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul le_radius_of_bound_nnreal tsum_fintype SummationFilter.instLeAtTopUnconditional Finset.sum_mul mul_le_mul' NNReal.mulLeftMono covariant_swap_mul_of_covariant_mul nnnorm_sum_le le_rfl sigma_mk_injective
mem_compPartialSumSource_iff 📖	mathematical	—	Finset SetLike.instMembership Finset.instSetLike compPartialSumSource	—	—
mem_compPartialSumTarget_iff 📖	mathematical	—	Composition Finset SetLike.instMembership Finset.instSetLike compPartialSumTarget Composition.length Composition.blocksFun	—	—
removeZero_applyComposition 📖	mathematical	—	applyComposition removeZero CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup	—	IsTopologicalAddGroup.toContinuousAdd removeZero_of_pos LT.lt.trans_le zero_lt_one Nat.instZeroLEOneClass Composition.one_le_blocksFun
removeZero_comp_of_pos 📖	mathematical	—	comp removeZero CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup	—	IsTopologicalAddGroup.toContinuousAdd ContinuousMultilinearMap.ext Finset.sum_congr ContinuousMultilinearMap.sum_apply removeZero_of_pos Composition.length_pos_of_pos

HasFPowerSeriesAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	HasFPowerSeriesAt	HasFPowerSeriesAt FormalMultilinearSeries.comp Field.toCommRing NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield 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	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul hasFPowerSeriesWithinAt_univ HasFPowerSeriesWithinAt.comp

HasFPowerSeriesWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	HasFPowerSeriesWithinAt Set.MapsTo	HasFPowerSeriesWithinAt FormalMultilinearSeries.comp Field.toCommRing NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield 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	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul FormalMultilinearSeries.comp_summable_nnreal HasFPowerSeriesWithinOnBall.radius_pos inter_mem_nhdsWithin Metric.eball_mem_nhds HasFPowerSeriesWithinOnBall.r_pos ContinuousWithinAt.tendsto_nhdsWithin AnalyticWithinAt.continuousWithinAt_insert HasFPowerSeriesWithinOnBall.analyticWithinAt Set.MapsTo.insert EMetric.mem_nhdsWithin_iff Set.inter_comm le_trans min_le_right FormalMultilinearSeries.le_comp_radius_of_summable Metric.eball_subset_eball min_le_left edist_eq_enorm_sub add_sub_cancel_left sub_zero Filter.Tendsto.prodMk Filter.tendsto_id Filter.eventually_atTop instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat eq_sub_iff_add_eq' Finset.range_eq_Ico HasFPowerSeriesWithinOnBall.coeff_zero Finset.sum_eq_sum_Ico_succ_bot Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub HasSum.tendsto_sum_nat HasFPowerSeriesWithinOnBall.hasSum tendsto_const_nhds Filter.Tendsto.congr' HasFPowerSeriesWithinOnBall.tendsto_partialSum_prod add_sub_cancel Filter.Tendsto.comp Finset.sum_congr FormalMultilinearSeries.comp_partialSum tendsto_nhds_of_cauchySeq_of_subseq cauchySeq_finset_of_norm_bounded NNReal.summable_coe ContinuousMultilinearMap.le_opNorm Finset.prod_const Finset.card_fin mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing pow_le_pow_left₀ IsOrderedRing.toMulPosMono norm_nonneg le_of_lt edist_zero_right Metric.mem_eball coe_nnnorm NNReal.coe_le_coe enorm_le_coe Filter.atTop_neBot FormalMultilinearSeries.compPartialSumTarget_tendsto_atTop HasSum.sigma TopologicalSpace.PseudoMetrizableSpace.regularSpace PseudoEMetricSpace.pseudoMetrizableSpace ContinuousMultilinearMap.sum_apply hasSum_fintype SummationFilter.instLeAtTopUnconditional

HasFiniteFPowerSeriesAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	HasFiniteFPowerSeriesAt	HasFiniteFPowerSeriesAt FormalMultilinearSeries.comp Field.toCommRing NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield 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	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul HasFPowerSeriesAt.comp hasFPowerSeriesAt Finset.sum_eq_zero ContinuousMultilinearMap.ext le_or_gt finite Mathlib.Tactic.Contrapose.contrapose₁ Composition.sum_blocksFun eq_zero_or_pos Nat.instCanonicallyOrderedAdd mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono Finset.sum_lt_sum Nat.instIsOrderedCancelAddMonoid IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid LT.lt.le Finset.mem_univ Finset.sum_const Fintype.card_fin mul_le_mul_left covariant_swap_mul_of_covariant_mul Nat.instMulLeftMono le_of_lt ContinuousMultilinearMap.map_coord_zero

---

← Back to Index