OrdinaryHypergeometric

📁 Source: Mathlib/Analysis/SpecialFunctions/OrdinaryHypergeometric.lean

Statistics

Metric	Count
Definitions ordinaryHypergeometric, ordinaryHypergeometricCoefficient, ordinaryHypergeometricSeries, term₂F₁	4
Theorems ordinaryHypergeometricSeries_apply_eq, ordinaryHypergeometricSeries_apply_eq', ordinaryHypergeometricSeries_apply_zero, ordinaryHypergeometricSeries_eq_zero_iff, ordinaryHypergeometricSeries_eq_zero_of_neg_nat, ordinaryHypergeometricSeries_norm_div_succ_norm, ordinaryHypergeometricSeries_radius_eq_one, ordinaryHypergeometricSeries_symm, ordinaryHypergeometric_eq_tsum, ordinaryHypergeometric_radius_top_of_neg_nat₁, ordinaryHypergeometric_radius_top_of_neg_nat₂, ordinaryHypergeometric_radius_top_of_neg_nat₃, ordinaryHypergeometric_sum_eq, ordinaryHypergeometric_zero	14
Total	18

(root)

Definitions

Name	Category	Theorems
ordinaryHypergeometric 📖	CompOp	2 math math: ordinaryHypergeometric_eq_tsum, ordinaryHypergeometric_zero
ordinaryHypergeometricCoefficient 📖	CompOp	1 math math: ordinaryHypergeometricSeries_norm_div_succ_norm
ordinaryHypergeometricSeries 📖	CompOp	12 math math: ordinaryHypergeometric_sum_eq, binomialSeries_eq_ordinaryHypergeometricSeries, ordinaryHypergeometric_radius_top_of_neg_nat₃, ordinaryHypergeometricSeries_radius_eq_one, ordinaryHypergeometricSeries_symm, ordinaryHypergeometricSeries_apply_eq', ordinaryHypergeometricSeries_apply_zero, ordinaryHypergeometric_radius_top_of_neg_nat₂, ordinaryHypergeometricSeries_apply_eq, ordinaryHypergeometricSeries_eq_zero_iff, ordinaryHypergeometric_radius_top_of_neg_nat₁, ordinaryHypergeometricSeries_eq_zero_of_neg_nat
term₂F₁ 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ordinaryHypergeometricSeries_apply_eq 📖	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 ordinaryHypergeometricSeries Algebra.toSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Nat.factorial Polynomial.eval ascPochhammer Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul ordinaryHypergeometricSeries.eq_1 FormalMultilinearSeries.ofScalars_apply_eq
ordinaryHypergeometricSeries_apply_eq' 📖	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 ordinaryHypergeometricSeries Algebra.toSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Nat.factorial Polynomial.eval ascPochhammer Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul ordinaryHypergeometricSeries.eq_1 FormalMultilinearSeries.ofScalars_apply_eq'
ordinaryHypergeometricSeries_apply_zero 📖	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 ordinaryHypergeometricSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Pi.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul ordinaryHypergeometricSeries.eq_1 FormalMultilinearSeries.ofScalars_apply_eq ordinaryHypergeometricCoefficient.eq_1 Nat.cast_one inv_one Polynomial.eval_one mul_one pow_zero one_smul Pi.single_eq_same zero_pow smul_zero Pi.single_eq_of_ne
ordinaryHypergeometricSeries_eq_zero_iff 📖	mathematical	—	ordinaryHypergeometricSeries NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NormedRing.toRing NormedDivisionRing.toNormedRing NormedAlgebra.toAlgebra NormedRing.toSeminormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Semifield.toCommSemiring Ring.toSemiring ContinuousMultilinearMap.instZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedCommRing.toNormedRing NormedField.toNormedCommRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass FormalMultilinearSeries.ofScalars_eq_zero IsSimpleRing.instNontrivial DivisionRing.isSimpleRing IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul ordinaryHypergeometricSeries.eq_1 RCLike.charZero_rclike ascPochhammer_eval_eq_zero_iff instIsDomain ordinaryHypergeometricSeries_eq_zero_of_neg_nat
ordinaryHypergeometricSeries_eq_zero_of_neg_nat 📖	mathematical	AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	ordinaryHypergeometricSeries ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Semifield.toCommSemiring Ring.toSemiring ContinuousMultilinearMap.instZero	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul ordinaryHypergeometricSeries.eq_1 FormalMultilinearSeries.ofScalars.eq_1 ContinuousMultilinearMap.ext instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero IsDomain.to_noZeroDivisors ascPochhammer_eval_eq_zero_iff MulZeroClass.mul_zero MulZeroClass.zero_mul inv_zero
ordinaryHypergeometricSeries_norm_div_succ_norm 📖	mathematical	—	Real DivInvMonoid.toDiv Real.instDivInvMonoid Norm.norm NormedField.toNorm DenselyNormedField.toNormedField RCLike.toDenselyNormedField ordinaryHypergeometricCoefficient NormedField.toField Real.instMul Real.instInv Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing AddMonoidWithOne.toOne	—	norm_mul NormedDivisionRing.toNormMulClass norm_inv Nat.cast_mul Nat.cast_add Nat.cast_one mul_inv_rev ascPochhammer_succ_eval Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.atom_pf 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 RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul 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.RingNF.nat_rawCast_1 pow_one mul_one add_zero Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.RingNF.mul_assoc_rev inv_inv DivisionRing.mul_inv_cancel norm_ne_zero_iff Iff.not ascPochhammer_eval_eq_zero_iff instIsDomain Mathlib.Tactic.Push.not_and_eq one_mul Nat.cast_ne_zero Nat.factorial_ne_zero
ordinaryHypergeometricSeries_radius_eq_one 📖	mathematical	—	FormalMultilinearSeries.radius DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedDivisionRing.toNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing ordinaryHypergeometricSeries NormedField.toField DenselyNormedField.toNormedField NormedRing.toRing NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing NonUnitalSeminormedRing.toIsTopologicalRing IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul FormalMultilinearSeries.ofScalars_radius_eq_of_tendsto NormedDivisionRing.to_normOneClass one_ne_zero NeZero.charZero_one IsStrictOrderedRing.toCharZero NNReal.instIsStrictOrderedRing Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf 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_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.atom_pf' Filter.Tendsto.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring div_self RCLike.charZero_rclike tendsto_add_mul_div_add_mul_atTop_nhds NNRat.instContinuousSMulOfIsScalarTowerOfRat IsScalarTower.nnrat Rat.instCharZero IsBoundedSMul.continuousSMul IsTopologicalDivisionRing.toContinuousInv₀ ordinaryHypergeometricSeries_norm_div_succ_norm NormedDivisionRing.toNormMulClass NormOneClass.norm_one Filter.Tendsto.norm
ordinaryHypergeometricSeries_symm 📖	mathematical	—	ordinaryHypergeometricSeries	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul mul_assoc mul_left_comm
ordinaryHypergeometric_eq_tsum 📖	mathematical	—	ordinaryHypergeometric tsum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toSMul Semifield.toCommSemiring Field.toSemifield Ring.toSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Nat.factorial Polynomial.eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring ascPochhammer Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero SummationFilter.unconditional	—	ordinaryHypergeometric_sum_eq
ordinaryHypergeometric_radius_top_of_neg_nat₁ 📖	mathematical	—	FormalMultilinearSeries.radius DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedDivisionRing.toNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing ordinaryHypergeometricSeries NormedField.toField DenselyNormedField.toNormedField NormedRing.toRing NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedCommRing.toNormedRing Top.top ENNReal instTopENNReal	—	FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zero IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing ordinaryHypergeometricSeries_eq_zero_of_neg_nat neg_neg RCLike.charZero_rclike
ordinaryHypergeometric_radius_top_of_neg_nat₂ 📖	mathematical	—	FormalMultilinearSeries.radius DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedDivisionRing.toNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing ordinaryHypergeometricSeries NormedField.toField DenselyNormedField.toNormedField NormedRing.toRing NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedCommRing.toNormedRing Top.top ENNReal instTopENNReal	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul ordinaryHypergeometricSeries_symm ordinaryHypergeometric_radius_top_of_neg_nat₁
ordinaryHypergeometric_radius_top_of_neg_nat₃ 📖	mathematical	—	FormalMultilinearSeries.radius DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedDivisionRing.toNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing ordinaryHypergeometricSeries NormedField.toField DenselyNormedField.toNormedField NormedRing.toRing NormedAlgebra.toAlgebra UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedCommRing.toNormedRing Top.top ENNReal instTopENNReal	—	FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zero IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing ordinaryHypergeometricSeries_eq_zero_of_neg_nat neg_neg RCLike.charZero_rclike
ordinaryHypergeometric_sum_eq 📖	mathematical	—	FormalMultilinearSeries.sum 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 tsum Algebra.toSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Nat.factorial Polynomial.eval ascPochhammer Monoid.toNatPow SummationFilter.unconditional	—	tsum_congr ordinaryHypergeometricSeries_apply_eq
ordinaryHypergeometric_zero 📖	mathematical	—	ordinaryHypergeometric MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	ordinaryHypergeometric_eq_tsum ordinaryHypergeometricSeries_apply_zero tsum_pi_single

---

← Back to Index