FormalMultilinearSeries

📁 Source: Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean

Statistics

Metric	Count
Definitions compFormalMultilinearSeries, fpowerSeries, toFormalMultilinearSeries, FormalMultilinearSeries, coeff, compContinuousLinearMap, fslope, instAddCommGroup, pi, prod, removeZero, restrictScalars, shift, unshift, constFormalMultilinearSeries, instAddCommMonoidFormalMultilinearSeries, instInhabitedFormalMultilinearSeries, instModuleFormalMultilinearSeriesOfContinuousConstSMulOfSMulCommClass	18
Theorems compFormalMultilinearSeries_apply, compFormalMultilinearSeries_apply', fpowerSeries_apply_add_two, fpowerSeries_apply_one, fpowerSeries_apply_zero, add_apply, apply_eq_pow_smul_coeff, apply_eq_prod_smul_coeff, apply_eq_zero_of_lt_order, apply_order_ne_zero, apply_order_ne_zero', coeff_eq_zero, coeff_fslope, coeff_iterate_fslope, compContinuousLinearMap_apply, compContinuousLinearMap_comp, compContinuousLinearMap_id, congr_zero, ext, ext_iff, mkPiRing_coeff_eq, ne_iff, ne_zero_of_order_ne_zero, neg_apply, norm_apply_eq_norm_coef, order_eq_find, order_eq_find', order_eq_zero_iff, order_eq_zero_iff', order_zero, removeZero_coeff_succ, removeZero_coeff_zero, removeZero_of_pos, smul_apply, sub_apply, unshift_shift, zero_apply, compContinuousLinearMap_zero, constFormalMultilinearSeries_apply_of_nonzero, constFormalMultilinearSeries_apply_succ, constFormalMultilinearSeries_apply_zero, constFormalMultilinearSeries_zero	42
Total	60

ContinuousLinearMap

Definitions

Name	Category	Theorems
compFormalMultilinearSeries 📖	CompOp	6 math math: comp_hasFiniteFPowerSeriesOnBall, compFormalMultilinearSeries_apply', comp_hasFPowerSeriesWithinOnBall, compFormalMultilinearSeries_apply, FormalMultilinearSeries.radius_le_radius_continuousLinearMap_comp, comp_hasFPowerSeriesOnBall
fpowerSeries 📖	CompOp	7 math math: hasFPowerSeriesOnBall, hasFPowerSeriesAt, fpowerSeries_apply_zero, fpowerSeries_apply_add_two, hasFiniteFPowerSeriesOnBall, fpowerSeries_radius, fpowerSeries_apply_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compFormalMultilinearSeries_apply 📖	mathematical	—	compFormalMultilinearSeries compContinuousMultilinearMap	—	—
compFormalMultilinearSeries_apply' 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap ContinuousMultilinearMap.funLike compFormalMultilinearSeries ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring funLike	—	—
fpowerSeries_apply_add_two 📖	mathematical	—	fpowerSeries 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	—	—
fpowerSeries_apply_one 📖	mathematical	—	fpowerSeries DFunLike.coe LinearIsometryEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousLinearMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap toSeminormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousMultilinearMap.seminormedAddCommGroup' Fin.fintype module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.instModule EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm continuousMultilinearCurryFin1	—	—
fpowerSeries_apply_zero 📖	mathematical	—	fpowerSeries ContinuousMultilinearMap.uncurry0 DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule funLike	—	—

ContinuousMultilinearMap

Definitions

Name	Category	Theorems
toFormalMultilinearSeries 📖	CompOp	3 math math: changeOrigin_toFormalMultilinearSeries, hasFiniteFPowerSeriesOnBall, changeOriginSeries_support

FormalMultilinearSeries

Definitions

Name	Category	Theorems
coeff 📖	CompOp	17 math math: PeriodPair.coeff_weierstrassPExceptSeries, coeff_fslope, derivSeries_coeff_one, norm_apply_eq_norm_coef, coeff_eq_zero, coeff_ofScalars, mkPiRing_coeff_eq, apply_eq_pow_smul_coeff, PeriodPair.weierstrassPExcept_eq_tsum, PeriodPair.coeff_weierstrassPSeries, apply_eq_prod_smul_coeff, PeriodPair.weierstrassPSeries_hasSum, PeriodPair.weierstrassPExceptSeries_hasSum, coeff_iterate_fslope, ModularFormClass.qExpansionFormalMultilinearSeries_coeff, hasFPowerSeriesAt_iff', hasFPowerSeriesAt_iff
compContinuousLinearMap 📖	CompOp	21 math math: binomialSeries_eq_ordinaryHypergeometricSeries, radius_compNeg, HasFPowerSeriesOnBall.compContinuousLinearMap, nnnorm_compContinuousLinearMap_le, compContinuousLinearMap_zero, le_radius_compContinuousLinearMap, radius_compContinuousLinearMap_linearIsometryEquiv_eq, norm_compContinuousLinearMap_le, compContinuousLinearMap_id, compContinuousLinearMap_applyComposition, radius_compContinuousLinearMap_eq, HasFPowerSeriesWithinOnBall.compContinuousLinearMap, div_le_radius_compContinuousLinearMap, ofScalars_comp_neg_id, radius_compContinuousLinearMap_le, compContinuousLinearMap_comp, ofScalars_comp_neg, enorm_compContinuousLinearMap_le, HasFPowerSeriesWithinAt.compContinuousLinearMap, compContinuousLinearMap_apply, HasFPowerSeriesAt.compContinuousLinearMap
fslope 📖	CompOp	4 math math: coeff_fslope, HasFPowerSeriesAt.has_fpower_series_iterate_dslope_fslope, coeff_iterate_fslope, HasFPowerSeriesAt.has_fpower_series_dslope_fslope
instAddCommGroup 📖	CompOp	32 math math: HasFiniteFPowerSeriesAt.neg, ofScalars_series_eq_zero_of_scalar_zero, HasFPowerSeriesWithinAt.const_smul, HasFPowerSeriesAt.neg, radius_le_smul, HasFPowerSeriesOnBall.const_smul, ofScalars_series_of_subsingleton, ofScalars_sub, radius_smul_eq, HasFPowerSeriesWithinOnBall.sub, neg_apply, HasFPowerSeriesOnBall.neg, HasFPowerSeriesWithinAt.sub, radius_neg, HasFiniteFPowerSeriesOnBall.neg, HasFPowerSeriesWithinOnBall.const_smul, HasFPowerSeriesOnBall.sub, HasFTaylorSeriesUpToOn.add, zero_radius, HasFPowerSeriesAt.const_smul, HasFPowerSeriesAt.sub, sub_apply, HasFPowerSeriesWithinOnBall.neg, ofScalars_smul, HasFPowerSeriesWithinAt.neg, HasFiniteFPowerSeriesAt.sub, ofScalars_series_eq_zero, HasFPowerSeriesAt.eq_zero, HasFPowerSeriesAt.eq_zero_of_eventually, HasFPowerSeriesAt.locally_zero_iff, HasFiniteFPowerSeriesOnBall.sub, constFormalMultilinearSeries_zero
pi 📖	CompOp	11 math math: radius_pi_eq_iInf, hasFPowerSeriesOnBall_pi_iff, HasFPowerSeriesWithinAt.pi, hasFPowerSeriesAt_pi_iff, hasFPowerSeriesWithinAt_pi_iff, HasFPowerSeriesOnBall.pi, hasFPowerSeriesWithinOnBall_pi_iff, HasFPowerSeriesAt.pi, le_radius_pi, radius_pi_le, HasFPowerSeriesWithinOnBall.pi
prod 📖	CompOp	5 math math: HasFPowerSeriesWithinOnBall.prod, HasFPowerSeriesWithinAt.prod, HasFPowerSeriesOnBall.prod, HasFPowerSeriesAt.prod, radius_prod_eq_min
removeZero 📖	CompOp	8 math math: removeZero_coeff_zero, rightInv_removeZero, comp_removeZero, removeZero_comp_of_pos, removeZero_of_pos, removeZero_coeff_succ, leftInv_removeZero, removeZero_applyComposition
restrictScalars 📖	CompOp	5 math math: HasFPowerSeriesWithinOnBall.restrictScalars, HasFPowerSeriesOnBall.restrictScalars, HasFPowerSeriesAt.restrictScalars, HasFPowerSeriesWithinAt.restrictScalars, HasFTaylorSeriesUpToOn.restrictScalars
shift 📖	CompOp	7 math math: hasFTaylorSeriesUpToOn_top_iff_right, hasFTaylorSeriesUpToOn_succ_iff_right, hasFTaylorSeriesUpTo_succ_nat_iff_right, hasFTaylorSeriesUpToOn_succ_nat_iff_right, HasFTaylorSeriesUpToOn.shift_of_succ, radius_shift, unshift_shift
unshift 📖	CompOp	5 math math: HasFPowerSeriesOnBall.unshift, HasFPowerSeriesWithinOnBall.unshift, radius_unshift, HasFPowerSeriesWithinAt.unshift, unshift_shift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply 📖	mathematical	—	FormalMultilinearSeries AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instAddCommMonoidFormalMultilinearSeries ContinuousMultilinearMap ContinuousMultilinearMap.instAdd	—	—
apply_eq_pow_smul_coeff 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace ContinuousMultilinearMap.funLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Monoid.toNatPow coeff	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul apply_eq_prod_smul_coeff Finset.prod_const Fintype.card_fin
apply_eq_prod_smul_coeff 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace ContinuousMultilinearMap.funLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Finset.prod CommRing.toCommMonoid Field.toCommRing Finset.univ Fin.fintype coeff	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul mul_one MultilinearMap.map_smul_univ
apply_eq_zero_of_lt_order 📖	mathematical	order	ContinuousMultilinearMap ContinuousMultilinearMap.instZero	—	by_contra Nat.notMem_of_lt_sInf
apply_order_ne_zero 📖	—	—	—	—	Nat.sInf_mem ne_iff
apply_order_ne_zero' 📖	—	—	—	—	apply_order_ne_zero ne_zero_of_order_ne_zero
coeff_eq_zero 📖	mathematical	—	coeff NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace ContinuousMultilinearMap.instZero	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsBoundedSMul.continuousSMul mkPiRing_coeff_eq ContinuousMultilinearMap.mkPiRing_eq_zero_iff
coeff_fslope 📖	mathematical	—	coeff fslope	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Fin.cons_self_tail
coeff_iterate_fslope 📖	mathematical	—	coeff Nat.iterate FormalMultilinearSeries DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.toUniformContinuousConstSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul fslope	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul coeff_fslope add_assoc
compContinuousLinearMap_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap ContinuousMultilinearMap.funLike compContinuousLinearMap ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike	—	—
compContinuousLinearMap_comp 📖	mathematical	—	compContinuousLinearMap ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	—
compContinuousLinearMap_id 📖	mathematical	—	compContinuousLinearMap ContinuousLinearMap.id	—	—
congr_zero 📖	—	ContinuousMultilinearMap ContinuousMultilinearMap.instZero	—	—	—
ext 📖	—	—	—	—	—
ext_iff 📖	—	—	—	—	ext
mkPiRing_coeff_eq 📖	mathematical	—	ContinuousMultilinearMap.mkPiRing Fin.fintype Field.toCommRing NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing IsBoundedSMul.continuousSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction NormedSpace.toIsBoundedSMul coeff	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContinuousMultilinearMap.mkPiRing_apply_one_eq_self IsBoundedSMul.continuousSMul
ne_iff 📖	—	—	—	—	Function.ne_iff
ne_zero_of_order_ne_zero 📖	—	—	—	—	order_zero
neg_apply 📖	mathematical	—	FormalMultilinearSeries Ring.toSemiring AddCommGroup.toAddCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup ContinuousMultilinearMap ContinuousMultilinearMap.instNeg	—	IsTopologicalAddGroup.toContinuousAdd
norm_apply_eq_norm_coef 📖	mathematical	—	Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace ContinuousMultilinearMap.hasOpNorm' Fin.fintype NormedAddCommGroup.toNorm coeff	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsBoundedSMul.continuousSMul mkPiRing_coeff_eq ContinuousMultilinearMap.norm_mkPiRing
order_eq_find 📖	mathematical	—	order Nat.find ContinuousMultilinearMap ContinuousMultilinearMap.instZero	—	Lean.Meta.FastSubsingleton.elim Lean.Meta.instFastSubsingletonForall Lean.Meta.instFastSubsingletonDecidable Nat.sInf_def
order_eq_find' 📖	mathematical	—	order Nat.find ContinuousMultilinearMap FormalMultilinearSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidFormalMultilinearSeries ne_iff	—	order_eq_find ne_iff
order_eq_zero_iff 📖	mathematical	—	order	—	—
order_eq_zero_iff' 📖	mathematical	—	order FormalMultilinearSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidFormalMultilinearSeries	—	—
order_zero 📖	mathematical	—	order FormalMultilinearSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidFormalMultilinearSeries	—	Nat.sInf_empty
removeZero_coeff_succ 📖	mathematical	—	removeZero	—	—
removeZero_coeff_zero 📖	mathematical	—	removeZero ContinuousMultilinearMap ContinuousMultilinearMap.instZero	—	—
removeZero_of_pos 📖	mathematical	—	removeZero	—	—
smul_apply 📖	mathematical	—	FormalMultilinearSeries SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidFormalMultilinearSeries DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instModuleFormalMultilinearSeriesOfContinuousConstSMulOfSMulCommClass ContinuousMultilinearMap ContinuousMultilinearMap.instSMul	—	—
sub_apply 📖	mathematical	—	FormalMultilinearSeries Ring.toSemiring AddCommGroup.toAddCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup SubNegMonoid.toSub AddGroup.toSubNegMonoid instAddCommGroup ContinuousMultilinearMap ContinuousMultilinearMap.instSub	—	IsTopologicalAddGroup.toContinuousAdd
unshift_shift 📖	mathematical	—	shift unshift	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self RingHomIsometric.ids ContinuousLinearMap.topologicalAddGroup ContinuousLinearMap.continuousConstSMul ext LinearIsometryEquiv.apply_symm_apply RingHomInvPair.ids ContinuousLinearMap.smulCommClass
zero_apply 📖	mathematical	—	FormalMultilinearSeries AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidFormalMultilinearSeries ContinuousMultilinearMap ContinuousMultilinearMap.instZero	—	—

(root)

Definitions

Name	Category	Theorems
FormalMultilinearSeries 📖	CompOp	49 math math: FormalMultilinearSeries.smul_apply, HasFiniteFPowerSeriesAt.neg, FormalMultilinearSeries.ofScalars_series_eq_zero_of_scalar_zero, HasFPowerSeriesOnBall.add, HasFPowerSeriesWithinAt.const_smul, HasFPowerSeriesAt.neg, HasFPowerSeriesAt.add, FormalMultilinearSeries.radius_le_smul, HasFPowerSeriesOnBall.const_smul, FormalMultilinearSeries.ofScalars_series_of_subsingleton, FormalMultilinearSeries.ofScalars_add, FormalMultilinearSeries.ofScalars_sub, FormalMultilinearSeries.radius_smul_eq, HasFPowerSeriesWithinOnBall.sub, FormalMultilinearSeries.order_eq_zero_iff', FormalMultilinearSeries.neg_apply, HasFPowerSeriesOnBall.neg, HasFPowerSeriesWithinAt.sub, FormalMultilinearSeries.radius_neg, HasFiniteFPowerSeriesOnBall.neg, HasFPowerSeriesWithinOnBall.const_smul, HasFPowerSeriesOnBall.sub, HasFTaylorSeriesUpToOn.add, HasFPowerSeriesAt.has_fpower_series_iterate_dslope_fslope, FormalMultilinearSeries.zero_radius, HasFPowerSeriesAt.const_smul, HasFiniteFPowerSeriesOnBall.add, HasFPowerSeriesAt.sub, FormalMultilinearSeries.sub_apply, HasFiniteFPowerSeriesAt.add, HasFPowerSeriesWithinOnBall.neg, FormalMultilinearSeries.ofScalars_smul, HasFPowerSeriesWithinOnBall.add, FormalMultilinearSeries.min_radius_le_radius_add, HasFPowerSeriesWithinAt.neg, HasFiniteFPowerSeriesAt.sub, FormalMultilinearSeries.ofScalars_series_eq_zero, FormalMultilinearSeries.order_eq_find', HasFPowerSeriesWithinAt.add, FormalMultilinearSeries.coeff_iterate_fslope, HasFPowerSeriesAt.eq_zero, FormalMultilinearSeries.ofScalars_series_injective, HasFPowerSeriesAt.eq_zero_of_eventually, FormalMultilinearSeries.add_apply, FormalMultilinearSeries.zero_apply, HasFPowerSeriesAt.locally_zero_iff, HasFiniteFPowerSeriesOnBall.sub, constFormalMultilinearSeries_zero, FormalMultilinearSeries.order_zero
constFormalMultilinearSeries 📖	CompOp	10 math math: hasFPowerSeriesAt_const, hasFPowerSeriesOnBall_const, compContinuousLinearMap_zero, constFormalMultilinearSeries_apply_zero, hasFiniteFPowerSeriesOnBall_const, hasFiniteFPowerSeriesAt_const, constFormalMultilinearSeries_apply_of_nonzero, constFormalMultilinearSeries_apply_succ, constFormalMultilinearSeries_zero, FormalMultilinearSeries.constFormalMultilinearSeries_radius
instAddCommMonoidFormalMultilinearSeries 📖	CompOp	21 math math: FormalMultilinearSeries.smul_apply, HasFPowerSeriesOnBall.add, HasFPowerSeriesWithinAt.const_smul, HasFPowerSeriesAt.add, FormalMultilinearSeries.radius_le_smul, HasFPowerSeriesOnBall.const_smul, FormalMultilinearSeries.ofScalars_add, FormalMultilinearSeries.radius_smul_eq, FormalMultilinearSeries.order_eq_zero_iff', HasFPowerSeriesWithinOnBall.const_smul, HasFPowerSeriesAt.const_smul, HasFiniteFPowerSeriesOnBall.add, HasFiniteFPowerSeriesAt.add, FormalMultilinearSeries.ofScalars_smul, HasFPowerSeriesWithinOnBall.add, FormalMultilinearSeries.min_radius_le_radius_add, FormalMultilinearSeries.order_eq_find', HasFPowerSeriesWithinAt.add, FormalMultilinearSeries.add_apply, FormalMultilinearSeries.zero_apply, FormalMultilinearSeries.order_zero
instInhabitedFormalMultilinearSeries 📖	CompOp	—
instModuleFormalMultilinearSeriesOfContinuousConstSMulOfSMulCommClass 📖	CompOp	8 math math: FormalMultilinearSeries.smul_apply, HasFPowerSeriesWithinAt.const_smul, FormalMultilinearSeries.radius_le_smul, HasFPowerSeriesOnBall.const_smul, FormalMultilinearSeries.radius_smul_eq, HasFPowerSeriesWithinOnBall.const_smul, HasFPowerSeriesAt.const_smul, FormalMultilinearSeries.ofScalars_smul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compContinuousLinearMap_zero 📖	mathematical	—	FormalMultilinearSeries.compContinuousLinearMap 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 ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.zero constFormalMultilinearSeries ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DFunLike.coe ContinuousMultilinearMap ContinuousMultilinearMap.funLike Pi.instZero	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul FormalMultilinearSeries.ext ContinuousMultilinearMap.ext constFormalMultilinearSeries.congr_simp Matrix.zero_empty Unique.instSubsingleton Fin.isEmpty' ContinuousMultilinearMap.map_zero
constFormalMultilinearSeries_apply_of_nonzero 📖	mathematical	—	constFormalMultilinearSeries UniformContinuousConstSMul.to_continuousConstSMul PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule 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 SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap ContinuousMultilinearMap.instZero	—	UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup
constFormalMultilinearSeries_apply_succ 📖	mathematical	—	constFormalMultilinearSeries UniformContinuousConstSMul.to_continuousConstSMul PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule 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 SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap ContinuousMultilinearMap.instZero	—	UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup
constFormalMultilinearSeries_apply_zero 📖	mathematical	—	constFormalMultilinearSeries UniformContinuousConstSMul.to_continuousConstSMul PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule 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 SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousMultilinearMap.uncurry0	—	UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup
constFormalMultilinearSeries_zero 📖	mathematical	—	constFormalMultilinearSeries UniformContinuousConstSMul.to_continuousConstSMul PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule 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 SeminormedAddCommGroup.toIsTopologicalAddGroup FormalMultilinearSeries IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup FormalMultilinearSeries.instAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.toAddCommGroup	—	FormalMultilinearSeries.ext IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContinuousMultilinearMap.ext

---

← Back to Index