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` 📖	—	`AnalyticAt`	—	—	`analyticWithinAt_univ` `AnalyticWithinAt.comp`
`comp'` 📖	—	`AnalyticAt`	—	—	`comp`
`comp_analyticWithinAt` 📖	—	`AnalyticAt` `AnalyticWithinAt`	—	—	`AnalyticWithinAt.comp` `analyticWithinAt_univ` `Set.mapsTo_univ`
`comp_analyticWithinAt_of_eq` 📖	—	`AnalyticAt` `AnalyticWithinAt`	—	—	`comp_analyticWithinAt`
`comp_of_eq` 📖	—	`AnalyticAt`	—	—	`comp`
`comp_of_eq'` 📖	—	`AnalyticAt`	—	—	`comp_of_eq`

AnalyticOn

Theorems

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

AnalyticOnNhd

Theorems

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

AnalyticWithinAt

Theorems

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

CPolynomialAt

Theorems

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

CPolynomialOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`CPolynomialOn` `Set.MapsTo`	—	—	`comp'` `mono` `Set.mapsTo_iff_image_subset`
`comp'` 📖	—	`CPolynomialOn` `Set.image`	—	—	`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` `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` `List.map_ofFn`
`sizeUpTo_sizeUpTo_add` 📖	mathematical	`length` `blocksFun`	`sizeUpTo` `gather` `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` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `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	2 math math: `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` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `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` `NormedAddCommGroup.toAddCommGroup` `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` `instPartialOrderNNReal` `NNNorm.nnnorm` `ContinuousMultilinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Field.toCommRing` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `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` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Composition.length` `Finset.prod` `CommSemiring.toCommMonoid` `instCommSemiringNNReal` `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` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `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` `NormedAddCommGroup.toAddCommGroup` `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` `Finset.instMembership` `compPartialSumSource`	`Composition.blocksFun` `Composition` `compChangeOfVariables` `Composition.length` `compChangeOfVariables_length`	—	`compChangeOfVariables_length`
`compChangeOfVariables_length` 📖	mathematical	`Finset` `Finset.instMembership` `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`	`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` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `le_trans` `le_max_left`
`comp_assoc` 📖	mathematical	—	`comp` `Field.toCommRing` `NormedField.toField` `NontriviallyNormedField.toNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `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` `NormedAddCommGroup.toAddCommGroup` `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` `Finset.sum_singleton` `compAlongComposition_apply` `Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForallOfFastIsEmpty` `Lean.Meta.instFastIsEmptyFinOfNatNat`
`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` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `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` `NormedAddCommGroup.toAddCommGroup` `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` `SeminormedAddCommGroup.toAddCommGroup` `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` `instPartialOrderNNReal` `instZeroNNReal` `Summable` `Composition` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNReal.instTopologicalSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NNNorm.nnnorm` `ContinuousMultilinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Field.toCommRing` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `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` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `Monoid.toNatPow` `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.instIsStrictOrderedRing` `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₀` `NNReal.instIsOrderedRing` `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` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `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`
`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` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `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` `NormedAddCommGroup.toAddCommGroup` `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` `SeminormedAddCommGroup.toAddCommGroup` `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` `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` `instSemiringNNReal` `NNReal.instTopologicalSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NNNorm.nnnorm` `ContinuousMultilinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Field.toCommRing` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `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` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `Monoid.toNatPow` `SummationFilter.unconditional`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal` `radius` `comp`	—	`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` `Finset.instMembership` `compPartialSumSource`	—	—
`mem_compPartialSumTarget_iff` 📖	mathematical	—	`Composition` `Finset` `Finset.instMembership` `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`	`FormalMultilinearSeries.comp` `Field.toCommRing` `NormedField.toField` `NontriviallyNormedField.toNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `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` `NormedAddCommGroup.toAddCommGroup` `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`	`FormalMultilinearSeries.comp` `Field.toCommRing` `NormedField.toField` `NontriviallyNormedField.toNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `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` `NormedAddCommGroup.toAddCommGroup` `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`	`FormalMultilinearSeries.comp` `Field.toCommRing` `NormedField.toField` `NontriviallyNormedField.toNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `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` `NormedAddCommGroup.toAddCommGroup` `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` `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