Binomial

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

Statistics

Metric	Count
Definitions binomialSeries	1
Theorems hasFPowerSeriesOnBall_ofScalars_mul_add_zero, ofReal_choose, one_add_cpow_hasFPowerSeriesAt_zero, one_add_cpow_hasFPowerSeriesOnBall_zero, one_div_one_sub_cpow_hasFPowerSeriesOnBall_zero, one_div_one_sub_hasFPowerSeriesOnBall_zero, one_div_one_sub_pow_hasFPowerSeriesOnBall_zero, one_div_one_sub_sq_hasFPowerSeriesOnBall_zero, one_div_sub_hasFPowerSeriesOnBall_zero, one_div_sub_pow_hasFPowerSeriesOnBall_zero, one_div_sub_sq_hasFPowerSeriesOnBall_zero, one_div_sub_sq_sub_one_div_sq_hasFPowerSeriesOnBall_zero, hasFPowerSeriesOnBall_linear_zero, hasFPowerSeriesOnBall_ofScalars_mul_add_zero, one_add_rpow_hasFPowerSeriesAt_zero, one_add_rpow_hasFPowerSeriesOnBall_zero, one_div_one_sub_hasFPowerSeriesOnBall_zero, one_div_one_sub_rpow_hasFPowerSeriesOnBall_zero, one_div_one_sub_sq_hasFPowerSeriesOnBall_zero, one_div_sub_hasFPowerSeriesOnBall_zero, one_div_sub_pow_hasFPowerSeriesOnBall_zero, one_div_sub_sq_hasFPowerSeriesOnBall_zero, binomialSeries_apply, binomialSeries_eq_ordinaryHypergeometricSeries, binomialSeries_radius_eq_one, binomialSeries_radius_eq_top_of_nat, binomialSeries_radius_ge_one, one_add_cpow_hasFPowerSeriesAt_zero, one_add_cpow_hasFPowerSeriesOnBall_zero, one_add_rpow_hasFPowerSeriesAt_zero, one_add_rpow_hasFPowerSeriesOnBall_zero	31
Total	32

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasFPowerSeriesOnBall_ofScalars_mul_add_zero 📖	mathematical	—	HasFPowerSeriesOnBall Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField instNormedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace instAdd DivInvMonoid.toDiv instDivInvMonoid instSub instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring FormalMultilinearSeries.ofScalars instField instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing instMul instNatCast instZero ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Algebra.to_smulCommClass div_eq_mul_inv one_mul FormalMultilinearSeries.ext IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul IsTopologicalSemiring.toContinuousMul ContinuousMultilinearMap.ext_ring Finite.of_fintype FormalMultilinearSeries.apply_eq_prod_smul_coeff Finset.prod_const_one FormalMultilinearSeries.coeff_ofScalars mul_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add HasFPowerSeriesOnBall.add HasFPowerSeriesOnBall.const_smul one_div_one_sub_hasFPowerSeriesOnBall_zero one_div_one_sub_sq_hasFPowerSeriesOnBall_zero
ofReal_choose 📖	mathematical	—	ofReal Ring.choose Real NonAssocRing.toAddCommGroupWithOne NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Real.commRing Monoid.toNatPow Real.instMonoid instBinomialRingOfModuleNNRat AddCommMonoidWithOne.toAddCommMonoid AddCommGroupWithOne.toAddCommMonoidWithOne Algebra.toModule NNRat instCommSemiringNNRat Real.semiring DivisionSemiring.toNNRatAlgebra Semifield.toDivisionSemiring Field.toSemifield Real.instField RCLike.charZero_rclike Real.instRCLike Complex commRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring instField instCharZero	—	Ring.map_choose RCLike.charZero_rclike instCharZero RingHom.instRingHomClass
one_add_cpow_hasFPowerSeriesAt_zero 📖	mathematical	—	HasFPowerSeriesAt Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField instNormedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace instPow instAdd instOne binomialSeries instField instCharZero instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing instZero	—	HasFPowerSeriesOnBall.hasFPowerSeriesAt instCharZero IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing one_add_cpow_hasFPowerSeriesOnBall_zero
one_add_cpow_hasFPowerSeriesOnBall_zero 📖	mathematical	—	HasFPowerSeriesOnBall Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField instNormedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace instPow instAdd instOne binomialSeries instField instCharZero instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing instZero ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul instCharZero instNontrivial eq_div_iff_mul_eq nsmul_eq_mul' Ring.descPochhammer_eq_factorial_smul_choose Monoid.PowAssoc iteratedDerivWithin_zero Polynomial.smeval_one pow_zero one_smul CharP.cast_eq_zero CharP.ofCharZero sub_zero one_mul iteratedDerivWithin_succ derivWithin_congr Set.EqOn.trans derivWithin_of_isOpen Metric.isOpen_ball deriv_const_mul_field' Nat.cast_add Nat.cast_one deriv_cpow_const DifferentiableAt.const_add differentiableAt_id mem_slitPlane_of_norm_lt_one dist_zero_right deriv_const_add' deriv_id'' mul_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add mul_assoc descPochhammer_succ_right Polynomial.smeval_mul IsScalarTower.right Polynomial.smeval_sub Polynomial.smeval_X pow_one Polynomial.smeval_natCast nsmul_eq_mul add_zero one_cpow iteratedDerivWithin_of_isOpen dist_self Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul AnalyticOn.hasFPowerSeriesOnSubball Mathlib.Meta.NormNum.isNat_lt_true ENNReal.instIsOrderedRing ENNReal.instCharZero Nat.cast_zero AnalyticOn.cpow AnalyticOn.add analyticOn_const analyticOn_id Metric.eball_ofReal ENNReal.ofReal_one binomialSeries_radius_ge_one
one_div_one_sub_cpow_hasFPowerSeriesOnBall_zero 📖	mathematical	—	HasFPowerSeriesOnBall Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField instNormedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace DivInvMonoid.toDiv instDivInvMonoid instOne instPow instSub FormalMultilinearSeries.ofScalars instField instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Ring.choose NonAssocRing.toAddCommGroupWithOne NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing commRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring instBinomialRingOfModuleNNRat AddCommMonoidWithOne.toAddCommMonoid AddCommGroupWithOne.toAddCommMonoidWithOne Algebra.toModule NNRat instCommSemiringNNRat DivisionSemiring.toNNRatAlgebra Semifield.toDivisionSemiring instCharZero instAdd instNatCast instZero ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul instCharZero SeminormedAddCommGroup.toIsTopologicalAddGroup FormalMultilinearSeries.ext ContinuousMultilinearMap.ext_ring Finite.of_fintype FormalMultilinearSeries.ofScalars.congr_simp Ring.choose_neg Monoid.PowAssoc Int.coe_negOnePow_natCast zsmul_eq_mul Int.cast_pow Int.cast_neg Int.cast_one FormalMultilinearSeries.apply_eq_prod_smul_coeff Finset.prod_const Fintype.card_fin FormalMultilinearSeries.coeff_ofScalars Even.neg_pow one_pow one_mul Finset.prod_const_one neg_zero one_add_cpow_hasFPowerSeriesOnBall_zero IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul one_div RingHomIsometric.ids cpow_neg enorm_neg enorm_one ContinuousLinearMap.normOneClass EMetric.instNontrivialTopologyOfNontrivial instNontrivial div_one HasFPowerSeriesOnBall.compContinuousLinearMap
one_div_one_sub_hasFPowerSeriesOnBall_zero 📖	mathematical	—	HasFPowerSeriesOnBall Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField instNormedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace DivInvMonoid.toDiv instDivInvMonoid instOne instSub FormalMultilinearSeries.ofScalars instField instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Pi.instOne instZero ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul one_div NeZero.charZero_one instCharZero one_pow inv_one enorm_one NormedDivisionRing.to_normOneClass one_div_sub_hasFPowerSeriesOnBall_zero
one_div_one_sub_pow_hasFPowerSeriesOnBall_zero 📖	mathematical	—	HasFPowerSeriesOnBall Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField instNormedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace DivInvMonoid.toDiv instDivInvMonoid instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring instSub FormalMultilinearSeries.ofScalars instField instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing instNatCast Nat.choose instZero ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing instCharZero IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Nat.cast_one cpow_natCast IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul add_right_comm add_sub_cancel_right Nat.cast_add Ring.choose_natCast Monoid.PowAssoc Nat.choose_symm_add one_div_one_sub_cpow_hasFPowerSeriesOnBall_zero
one_div_one_sub_sq_hasFPowerSeriesOnBall_zero 📖	mathematical	—	HasFPowerSeriesOnBall Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField instNormedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace DivInvMonoid.toDiv instDivInvMonoid instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring instSub FormalMultilinearSeries.ofScalars instField instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing instAdd instNatCast instZero ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul one_div NeZero.charZero_one instCharZero one_pow inv_one one_mul enorm_one NormedDivisionRing.to_normOneClass one_div_sub_sq_hasFPowerSeriesOnBall_zero
one_div_sub_hasFPowerSeriesOnBall_zero 📖	mathematical	—	HasFPowerSeriesOnBall Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField instNormedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace DivInvMonoid.toDiv instDivInvMonoid instOne instSub FormalMultilinearSeries.ofScalars instField instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing instInv Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring instZero ENorm.enorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing SeminormedAddGroup.toContinuousENorm	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul one_div zero_add pow_one add_zero Nat.choose_zero_right Nat.cast_one mul_one one_div_sub_pow_hasFPowerSeriesOnBall_zero
one_div_sub_pow_hasFPowerSeriesOnBall_zero 📖	mathematical	—	HasFPowerSeriesOnBall Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField instNormedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace DivInvMonoid.toDiv instDivInvMonoid instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring instSub FormalMultilinearSeries.ofScalars instField instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing instMul instInv instNatCast Nat.choose instZero ENorm.enorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing SeminormedAddGroup.toContinuousENorm	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing one_div_one_sub_pow_hasFPowerSeriesOnBall_zero Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomIsometric.ids HasFPowerSeriesOnBall.compContinuousLinearMap map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass enorm_smul instENormSMulClass NormedSpace.toNormSMulClass enorm_inv enorm_one ContinuousLinearMap.normOneClass EMetric.instNontrivialTopologyOfNontrivial instNontrivial mul_one one_div inv_inv FormalMultilinearSeries.ext IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul ContinuousMultilinearMap.ext_ring Finite.of_fintype FormalMultilinearSeries.ofScalars.congr_simp add_assoc pow_add mul_inv_rev mul_assoc FormalMultilinearSeries.apply_eq_prod_smul_coeff Finset.prod_const_one FormalMultilinearSeries.coeff_ofScalars one_mul Finset.prod_congr Finset.prod_inv_distrib Finset.prod_const Fintype.card_fin HasFPowerSeriesOnBall.congr HasFPowerSeriesOnBall.const_smul sub_mul mul_right_comm inv_mul_cancel₀
one_div_sub_sq_hasFPowerSeriesOnBall_zero 📖	mathematical	—	HasFPowerSeriesOnBall Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField instNormedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace DivInvMonoid.toDiv instDivInvMonoid instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring instSub FormalMultilinearSeries.ofScalars instField instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing instMul instInv instAdd instNatCast instZero ENorm.enorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing SeminormedAddGroup.toContinuousENorm	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul one_div add_comm Nat.choose_one_right Nat.cast_add Nat.cast_one one_div_sub_pow_hasFPowerSeriesOnBall_zero
one_div_sub_sq_sub_one_div_sq_hasFPowerSeriesOnBall_zero 📖	mathematical	—	HasFPowerSeriesOnBall Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField instNormedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace instSub DivInvMonoid.toDiv instDivInvMonoid instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring FormalMultilinearSeries.ofScalars instField instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing instMul instAdd instNatCast DivInvMonoid.toZPow Pi.instZero instZero ENorm.enorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing SeminormedAddGroup.toContinuousENorm	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Pi.sub_def IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalRing.to_topologicalAddGroup FormalMultilinearSeries.ofScalars_sub HasFPowerSeriesOnBall.sub zpow_neg zpow_natCast IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul sub_sub_sub_cancel_right sub_sq_comm mul_comm zero_add HasFPowerSeriesOnBall.comp_sub one_div_sub_sq_hasFPowerSeriesOnBall_zero FormalMultilinearSeries.ext ContinuousMultilinearMap.ext_ring Finite.of_fintype FormalMultilinearSeries.ofScalars.congr_simp zpow_ofNat FormalMultilinearSeries.apply_eq_prod_smul_coeff Finset.prod_congr Finset.univ_eq_empty Fin.isEmpty' Finset.prod_const_one FormalMultilinearSeries.coeff_ofScalars one_mul constFormalMultilinearSeries.congr_simp one_div FormalMultilinearSeries.ofScalars_eq_zero_of_scalar_zero HasFPowerSeriesOnBall.mono hasFPowerSeriesOnBall_const le_top

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasFPowerSeriesOnBall_linear_zero 📖	mathematical	—	HasFPowerSeriesOnBall Real DenselyNormedField.toNontriviallyNormedField denselyNormedField normedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal instAdd DivInvMonoid.toDiv instDivInvMonoid instSub instOne Monoid.toNatPow instMonoid FormalMultilinearSeries.ofScalars instField instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instIsTopologicalRingReal instMul instNatCast instZero ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	hasFPowerSeriesOnBall_ofScalars_mul_add_zero
hasFPowerSeriesOnBall_ofScalars_mul_add_zero 📖	mathematical	—	HasFPowerSeriesOnBall Real DenselyNormedField.toNontriviallyNormedField denselyNormedField normedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal instAdd DivInvMonoid.toDiv instDivInvMonoid instSub instOne Monoid.toNatPow instMonoid FormalMultilinearSeries.ofScalars instField instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instIsTopologicalRingReal instMul instNatCast instZero ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	instIsTopologicalRingReal IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul isBoundedSMul Algebra.to_smulCommClass div_eq_mul_inv one_mul FormalMultilinearSeries.ext IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul IsTopologicalSemiring.toContinuousMul ContinuousMultilinearMap.ext_ring Finite.of_fintype FormalMultilinearSeries.apply_eq_prod_smul_coeff Finset.prod_const_one FormalMultilinearSeries.coeff_ofScalars mul_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add HasFPowerSeriesOnBall.add HasFPowerSeriesOnBall.const_smul one_div_one_sub_hasFPowerSeriesOnBall_zero one_div_one_sub_sq_hasFPowerSeriesOnBall_zero
one_add_rpow_hasFPowerSeriesAt_zero 📖	mathematical	—	HasFPowerSeriesAt Real DenselyNormedField.toNontriviallyNormedField denselyNormedField normedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal instPow instAdd instOne binomialSeries instField RCLike.charZero_rclike instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instIsTopologicalRingReal instZero	—	HasFPowerSeriesOnBall.hasFPowerSeriesAt RCLike.charZero_rclike instIsTopologicalRingReal one_add_rpow_hasFPowerSeriesOnBall_zero
one_add_rpow_hasFPowerSeriesOnBall_zero 📖	mathematical	—	HasFPowerSeriesOnBall Real DenselyNormedField.toNontriviallyNormedField denselyNormedField normedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal instPow instAdd instOne binomialSeries instField RCLike.charZero_rclike instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instIsTopologicalRingReal instZero ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul RCLike.charZero_rclike UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsScalarTower.right Complex.instCharZero FormalMultilinearSeries.ext ContinuousMultilinearMap.ext binomialSeries_apply HasFPowerSeriesOnBall.restrictScalars Complex.one_add_cpow_hasFPowerSeriesOnBall_zero ContinuousLinearMap.map_zero instIsTopologicalRingReal IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomIsometric.ids ContinuousMultilinearMap.ext_ring Finite.of_fintype List.ofFn_const List.prod_replicate one_pow mul_one ContinuousLinearMap.compContinuousMultilinearMap_coe Complex.ofRealCLM_enorm div_one HasFPowerSeriesOnBall.congr ContinuousLinearMap.comp_hasFPowerSeriesOnBall HasFPowerSeriesOnBall.compContinuousLinearMap Nat.cast_one
one_div_one_sub_hasFPowerSeriesOnBall_zero 📖	mathematical	—	HasFPowerSeriesOnBall Real DenselyNormedField.toNontriviallyNormedField denselyNormedField normedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal DivInvMonoid.toDiv instDivInvMonoid instOne instSub FormalMultilinearSeries.ofScalars instField instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instIsTopologicalRingReal Pi.instOne instZero ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	instIsTopologicalRingReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul one_div NeZero.charZero_one RCLike.charZero_rclike one_pow inv_one enorm_one NormedDivisionRing.to_normOneClass one_div_sub_hasFPowerSeriesOnBall_zero
one_div_one_sub_rpow_hasFPowerSeriesOnBall_zero 📖	mathematical	—	HasFPowerSeriesOnBall Real DenselyNormedField.toNontriviallyNormedField denselyNormedField normedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal DivInvMonoid.toDiv instDivInvMonoid instOne instPow instSub FormalMultilinearSeries.ofScalars instField instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instIsTopologicalRingReal Ring.choose NonAssocRing.toAddCommGroupWithOne NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing commRing Monoid.toNatPow instMonoid instBinomialRingOfModuleNNRat AddCommMonoidWithOne.toAddCommMonoid AddCommGroupWithOne.toAddCommMonoidWithOne Algebra.toModule NNRat instCommSemiringNNRat semiring DivisionSemiring.toNNRatAlgebra Semifield.toDivisionSemiring RCLike.charZero_rclike instAdd instNatCast instZero ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsScalarTower.right IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instCharZero HasFPowerSeriesOnBall.restrictScalars Complex.one_div_one_sub_cpow_hasFPowerSeriesOnBall_zero instIsTopologicalRingReal RCLike.charZero_rclike RingHomIsometric.ids FormalMultilinearSeries.ext IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul ContinuousMultilinearMap.ext_ring Finite.of_fintype ContinuousLinearMap.compContinuousMultilinearMap_coe FormalMultilinearSeries.apply_eq_prod_smul_coeff Finset.prod_const_one FormalMultilinearSeries.coeff_ofScalars one_mul Finset.prod_congr Nat.cast_one Complex.ofRealCLM_enorm div_one HasFPowerSeriesOnBall.congr ContinuousLinearMap.comp_hasFPowerSeriesOnBall HasFPowerSeriesOnBall.compContinuousLinearMap ContinuousLinearMap.map_zero Complex.ofRealCLM_nnnorm edist_zero_right Complex.ofReal_cpow Complex.div_ofReal_re one_div
one_div_one_sub_sq_hasFPowerSeriesOnBall_zero 📖	mathematical	—	HasFPowerSeriesOnBall Real DenselyNormedField.toNontriviallyNormedField denselyNormedField normedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal DivInvMonoid.toDiv instDivInvMonoid instOne Monoid.toNatPow instMonoid instSub FormalMultilinearSeries.ofScalars instField instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instIsTopologicalRingReal instAdd instNatCast instZero ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	instIsTopologicalRingReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul one_div NeZero.charZero_one RCLike.charZero_rclike one_pow inv_one one_mul enorm_one NormedDivisionRing.to_normOneClass one_div_sub_sq_hasFPowerSeriesOnBall_zero
one_div_sub_hasFPowerSeriesOnBall_zero 📖	mathematical	—	HasFPowerSeriesOnBall Real DenselyNormedField.toNontriviallyNormedField denselyNormedField normedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal DivInvMonoid.toDiv instDivInvMonoid instOne instSub FormalMultilinearSeries.ofScalars instField instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instIsTopologicalRingReal instInv Monoid.toNatPow instMonoid instZero ENorm.enorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing SeminormedAddGroup.toContinuousENorm	—	instIsTopologicalRingReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul one_div zero_add pow_one add_zero Nat.choose_zero_right Nat.cast_one mul_one one_div_sub_pow_hasFPowerSeriesOnBall_zero
one_div_sub_pow_hasFPowerSeriesOnBall_zero 📖	mathematical	—	HasFPowerSeriesOnBall Real DenselyNormedField.toNontriviallyNormedField denselyNormedField normedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal DivInvMonoid.toDiv instDivInvMonoid instOne Monoid.toNatPow instMonoid instSub FormalMultilinearSeries.ofScalars instField instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instIsTopologicalRingReal instMul instInv instNatCast Nat.choose instZero ENorm.enorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing SeminormedAddGroup.toContinuousENorm	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsScalarTower.right IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing HasFPowerSeriesOnBall.restrictScalars Complex.one_div_sub_pow_hasFPowerSeriesOnBall_zero instIsTopologicalRingReal RingHomIsometric.ids one_div FormalMultilinearSeries.ext IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul ContinuousMultilinearMap.ext_ring Finite.of_fintype ContinuousLinearMap.compContinuousMultilinearMap_coe FormalMultilinearSeries.apply_eq_prod_smul_coeff Finset.prod_const_one FormalMultilinearSeries.coeff_ofScalars one_mul ContinuousMultilinearMap.restrictScalars.congr_simp FormalMultilinearSeries.ofScalars.congr_simp Finset.prod_congr MulZeroClass.mul_zero sub_zero Complex.nnnorm_real Complex.ofRealCLM_nnnorm div_one ContinuousLinearMap.comp_hasFPowerSeriesOnBall HasFPowerSeriesOnBall.compContinuousLinearMap ContinuousLinearMap.map_zero
one_div_sub_sq_hasFPowerSeriesOnBall_zero 📖	mathematical	—	HasFPowerSeriesOnBall Real DenselyNormedField.toNontriviallyNormedField denselyNormedField normedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal DivInvMonoid.toDiv instDivInvMonoid instOne Monoid.toNatPow instMonoid instSub FormalMultilinearSeries.ofScalars instField instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instIsTopologicalRingReal instMul instInv instAdd instNatCast instZero ENorm.enorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing SeminormedAddGroup.toContinuousENorm	—	instIsTopologicalRingReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul one_div add_comm Nat.choose_one_right Nat.cast_add Nat.cast_one one_div_sub_pow_hasFPowerSeriesOnBall_zero

(root)

Definitions

Name	Category	Theorems
binomialSeries 📖	CompOp	13 math math: binomialSeries_eq_ordinaryHypergeometricSeries, one_add_cpow_hasFPowerSeriesAt_zero, Real.one_add_rpow_hasFPowerSeriesOnBall_zero, binomialSeries_radius_eq_one, binomialSeries_apply, Complex.one_add_cpow_hasFPowerSeriesAt_zero, binomialSeries_radius_eq_top_of_nat, Real.one_add_rpow_hasFPowerSeriesAt_zero, one_add_rpow_hasFPowerSeriesAt_zero, one_add_cpow_hasFPowerSeriesOnBall_zero, Complex.one_add_cpow_hasFPowerSeriesOnBall_zero, one_add_rpow_hasFPowerSeriesOnBall_zero, binomialSeries_radius_ge_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
binomialSeries_apply 📖	mathematical	—	DFunLike.coe ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Semifield.toCommSemiring Ring.toSemiring ContinuousMultilinearMap.funLike binomialSeries Algebra.toSMul Ring.choose NonAssocRing.toAddCommGroupWithOne NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instBinomialRingOfModuleNNRat AddCommMonoidWithOne.toAddCommMonoid AddCommGroupWithOne.toAddCommMonoidWithOne NNRat instCommSemiringNNRat DivisionSemiring.toNNRatAlgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
binomialSeries_eq_ordinaryHypergeometricSeries 📖	mathematical	—	binomialSeries FormalMultilinearSeries.compContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Semifield.toCommSemiring Ring.toSemiring IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring ordinaryHypergeometricSeries NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.neg IsTopologicalRing.to_topologicalAddGroup ContinuousLinearMap.id	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalRing.to_topologicalAddGroup FormalMultilinearSeries.ofScalars_comp_neg_id ordinaryHypergeometricCoefficient.eq_1 mul_inv_cancel_right₀ instIsDomain Ring.choose_eq_smul Polynomial.descPochhammer_smeval_eq_ascPochhammer Monoid.PowAssoc Polynomial.ascPochhammer_smeval_cast IsScalarTower.right Polynomial.ascPochhammer_smeval_eq_eval ascPochhammer_eval_neg_eq_descPochhammer descPochhammer_eval_eq_ascPochhammer Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg add_zero Mathlib.Tactic.RingNF.add_neg Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.RingNF.mul_assoc_rev Even.neg_pow Distrib.leftDistribClass one_pow
binomialSeries_radius_eq_one 📖	mathematical	—	FormalMultilinearSeries.radius DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedDivisionRing.toNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing binomialSeries NormedField.toField DenselyNormedField.toNormedField RCLike.charZero_rclike NormedRing.toRing NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	RCLike.charZero_rclike IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalRing.to_topologicalAddGroup binomialSeries_eq_ordinaryHypergeometricSeries Nat.cast_one Int.cast_natCast FormalMultilinearSeries.radius_compNeg IsSimpleRing.instNontrivial DivisionRing.isSimpleRing ordinaryHypergeometricSeries_radius_eq_one
binomialSeries_radius_eq_top_of_nat 📖	mathematical	—	FormalMultilinearSeries.radius DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedDivisionRing.toNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing binomialSeries NormedField.toField DenselyNormedField.toNormedField RCLike.charZero_rclike NormedRing.toRing NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedCommRing.toNormedRing NormedField.toNormedCommRing Top.top ENNReal instTopENNReal	—	RCLike.charZero_rclike IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalRing.to_topologicalAddGroup binomialSeries_eq_ordinaryHypergeometricSeries Nat.cast_one Int.cast_natCast FormalMultilinearSeries.radius_compNeg IsSimpleRing.instNontrivial DivisionRing.isSimpleRing ordinaryHypergeometric_radius_top_of_neg_nat₁
binomialSeries_radius_ge_one 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal FormalMultilinearSeries.radius DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedDivisionRing.toNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing binomialSeries NormedField.toField DenselyNormedField.toNormedField RCLike.charZero_rclike NormedRing.toRing NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing	—	RCLike.charZero_rclike IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing binomialSeries_radius_eq_one le_refl Mathlib.Tactic.Push.not_forall_eq binomialSeries_radius_eq_top_of_nat
one_add_cpow_hasFPowerSeriesAt_zero 📖	mathematical	—	HasFPowerSeriesAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.instPow Complex.instAdd Complex.instOne binomialSeries Complex.instField Complex.instCharZero Complex.instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instZero	—	Complex.one_add_cpow_hasFPowerSeriesAt_zero
one_add_cpow_hasFPowerSeriesOnBall_zero 📖	mathematical	—	HasFPowerSeriesOnBall Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Complex.instPow Complex.instAdd Complex.instOne binomialSeries Complex.instField Complex.instCharZero Complex.instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instZero ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	Complex.one_add_cpow_hasFPowerSeriesOnBall_zero
one_add_rpow_hasFPowerSeriesAt_zero 📖	mathematical	—	HasFPowerSeriesAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instPow Real.instAdd Real.instOne binomialSeries Real.instField RCLike.charZero_rclike Real.instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instIsTopologicalRingReal Real.instZero	—	Real.one_add_rpow_hasFPowerSeriesAt_zero
one_add_rpow_hasFPowerSeriesOnBall_zero 📖	mathematical	—	HasFPowerSeriesOnBall Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instPow Real.instAdd Real.instOne binomialSeries Real.instField RCLike.charZero_rclike Real.instRing Algebra.id Semifield.toCommSemiring Field.toSemifield UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instIsTopologicalRingReal Real.instZero ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	Real.one_add_rpow_hasFPowerSeriesOnBall_zero

---

← Back to Index