Pochhammer

📁 Source: Mathlib/RingTheory/Polynomial/Pochhammer.lean

Statistics

Metric	Count
Definitions ascPochhammer, descPochhammer	2
Theorems cast_ascFactorial, cast_choose_eq_ascPochhammer_div, cast_choose_eq_descPochhammer_div, cast_descFactorial, cast_factorial, ascPochhammer_eval_cast, ascPochhammer_eval_comp, ascPochhammer_eval_eq_zero_iff, ascPochhammer_eval_neg_coe_nat_of_lt, ascPochhammer_eval_neg_eq_descPochhammer, ascPochhammer_eval_one, ascPochhammer_eval_succ, ascPochhammer_eval_zero, ascPochhammer_eval₂, ascPochhammer_map, ascPochhammer_mul, ascPochhammer_natDegree, ascPochhammer_nat_eq_ascFactorial, ascPochhammer_nat_eq_descFactorial, ascPochhammer_nat_eq_natCast_ascFactorial, ascPochhammer_nat_eq_natCast_descFactorial, ascPochhammer_nat_eval_succ, ascPochhammer_ne_zero_eval_zero, ascPochhammer_one, ascPochhammer_pos, ascPochhammer_succ_comp_X_add_one, ascPochhammer_succ_eval, ascPochhammer_succ_left, ascPochhammer_succ_right, ascPochhammer_zero, ascPochhammer_zero_eval_zero, descPochhammer_eq_ascPochhammer, descPochhammer_eval_cast, descPochhammer_eval_coe_nat_of_lt, descPochhammer_eval_eq_ascPochhammer, descPochhammer_eval_eq_descFactorial, descPochhammer_eval_eq_prod_range, descPochhammer_eval_zero, descPochhammer_int_eq_ascFactorial, descPochhammer_map, descPochhammer_mul, descPochhammer_natDegree, descPochhammer_ne_zero_eval_zero, descPochhammer_nonneg, descPochhammer_one, descPochhammer_pos, descPochhammer_succ_comp_X_sub_one, descPochhammer_succ_eval, descPochhammer_succ_left, descPochhammer_succ_right, descPochhammer_zero, descPochhammer_zero_eval_zero, factorial_mul_ascPochhammer, monic_ascPochhammer, monic_descPochhammer, monotoneOn_descPochhammer_eval, pow_le_descPochhammer_eval	57
Total	59

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_ascFactorial 📖	mathematical	—	AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring ascFactorial Polynomial.eval ascPochhammer	—	ascPochhammer_nat_eq_ascFactorial ascPochhammer_eval_cast
cast_choose_eq_ascPochhammer_div 📖	mathematical	—	AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring choose DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero Polynomial.eval ascPochhammer factorial	—	eq_div_iff_mul_eq cast_ne_zero factorial_ne_zero cast_mul mul_comm descFactorial_eq_factorial_mul_choose cast_descFactorial
cast_choose_eq_descPochhammer_div 📖	mathematical	—	AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing choose DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Polynomial.eval Ring.toSemiring descPochhammer factorial	—	eq_div_iff_mul_eq cast_ne_zero factorial_ne_zero cast_mul mul_comm descFactorial_eq_factorial_mul_choose descPochhammer_eval_eq_descFactorial
cast_descFactorial 📖	mathematical	—	AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring descFactorial Polynomial.eval ascPochhammer	—	ascPochhammer_eval_cast ascPochhammer_nat_eq_descFactorial cast_one zero_tsub instCanonicallyOrderedAdd instOrderedSub tsub_zero add_zero le_total descFactorial_of_lt tsub_eq_zero_iff_le zero_add le_refl tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
cast_factorial 📖	mathematical	—	AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring factorial Polynomial.eval AddMonoidWithOne.toOne ascPochhammer	—	one_ascFactorial cast_ascFactorial cast_one

(root)

Definitions

Name	Category	Theorems
ascPochhammer 📖	CompOp	54 math math: ascPochhammer_ne_zero_eval_zero, ordinaryHypergeometric_sum_eq, Polynomial.ascPochhammer_smeval_neg_eq_descPochhammer, Nat.cast_factorial, Nat.cast_choose_eq_ascPochhammer_div, ascPochhammer_one, ascPochhammer_succ_eval, ascPochhammer_eval_one, Nat.cast_ascFactorial, ascPochhammer_nat_eq_descFactorial, ascPochhammer_succ_comp_X_add_one, ascPochhammer_eval_zero, ascPochhammer_mul, PadicInt.norm_ascPochhammer_le, ordinaryHypergeometricSeries_apply_eq', ascPochhammer_nat_eq_natCast_descFactorial, Ring.factorial_nsmul_multichoose_eq_ascPochhammer, ascPochhammer_eval_eq_zero_iff, descPochhammer_eq_ascPochhammer, ascPochhammer_map, ordinaryHypergeometric_eq_tsum, monic_ascPochhammer, Ring.ascPochhammer_succ_succ, ordinaryHypergeometricSeries_apply_eq, BinomialRing.factorial_nsmul_multichoose, ascPochhammer_nat_eval_succ, ascPochhammer_natDegree, Ring.smeval_ascPochhammer_int_ofNat, ascPochhammer_eval_neg_coe_nat_of_lt, ascPochhammer_zero, Ring.smeval_ascPochhammer_nat_cast, ascPochhammer_pos, Polynomial.ascPochhammer_smeval_cast, ascPochhammer_eval_comp, Ring.smeval_ascPochhammer_neg_add, descPochhammer_eval_eq_ascPochhammer, ascPochhammer_zero_eval_zero, ascPochhammer_nat_eq_natCast_ascFactorial, ascPochhammer_eval_succ, Ring.smeval_ascPochhammer_succ_neg, Polynomial.ascPochhammer_smeval_eq_eval, ascPochhammer_eval_cast, Ring.smeval_ascPochhammer_neg_of_lt, ascPochhammer_nat_eq_ascFactorial, bernsteinPolynomial.iterate_derivative_at_0, Polynomial.descPochhammer_smeval_eq_ascPochhammer, Ring.smeval_ascPochhammer_self_neg, ascPochhammer_succ_left, ascPochhammer_eval₂, ascPochhammer_eval_neg_eq_descPochhammer, Nat.cast_descFactorial, ascPochhammer_succ_right, bernsteinPolynomial.iterate_derivative_at_1, factorial_mul_ascPochhammer
descPochhammer 📖	CompOp	42 math math: Polynomial.ascPochhammer_smeval_neg_eq_descPochhammer, descPochhammer_succ_comp_X_sub_one, differentiable_descPochhammer_eval, Ring.choose_eq_smul, descPochhammer_one, descPochhammer_ne_zero_eval_zero, monotoneOn_descPochhammer_eval, descPochhammer_eval_div_factorial_le_sum_choose, descPochhammer_succ_right, descPochhammer_eval_cast, LaurentSeries.derivative_iterate_coeff, Polynomial.descPochhammer_smeval_eq_descFactorial, descPochhammer_eval_le_sum_descFactorial, descPochhammer_map, monotoneOn_deriv_descPochhammer_eval, Ring.descPochhammer_smeval_add, descPochhammer_eq_ascPochhammer, descPochhammer_nonneg, Nat.cast_choose_eq_descPochhammer_div, convexOn_descPochhammer_eval, descPochhammer_succ_left, descPochhammer_mul, descPochhammer_int_eq_ascFactorial, descPochhammer_natDegree, descPochhammer_eval_eq_descFactorial, monic_descPochhammer, descPochhammer_eval_coe_nat_of_lt, pow_le_descPochhammer_eval, descPochhammer_pos, descPochhammer_eval_eq_ascPochhammer, descPochhammer_eval_eq_prod_range, Real.iter_deriv_rpow_const, descPochhammer_succ_eval, continuous_descPochhammer_eval, Ring.descPochhammer_eq_factorial_smul_choose, deriv_descPochhammer_eval_eq_sum_prod_range_erase, Ring.descPochhammer_succ_succ_smeval, descPochhammer_zero_eval_zero, descPochhammer_eval_zero, Polynomial.descPochhammer_smeval_eq_ascPochhammer, descPochhammer_zero, ascPochhammer_eval_neg_eq_descPochhammer

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ascPochhammer_eval_cast 📖	mathematical	—	AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Polynomial.eval Nat.instSemiring ascPochhammer	—	ascPochhammer_map Polynomial.eval_map eq_natCast RingHom.instRingHomClass Polynomial.eval₂_at_natCast Nat.cast_id
ascPochhammer_eval_comp 📖	mathematical	—	Polynomial.eval Polynomial.comp ascPochhammer Polynomial.map CommSemiring.toSemiring algebraMap Polynomial.eval₂	—	ascPochhammer_eval₂ Polynomial.eval₂_comp' ascPochhammer_map Polynomial.map_comp Polynomial.eval_map
ascPochhammer_eval_eq_zero_iff 📖	mathematical	—	Polynomial.eval Ring.toSemiring ascPochhammer MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	Polynomial.eval_one NeZero.one IsDomain.toNontrivial mul_eq_zero IsDomain.to_noZeroDivisors ascPochhammer_succ_eval lt_add_one Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid eq_neg_of_add_eq_zero_right neg_neg ascPochhammer_eval_neg_coe_nat_of_lt
ascPochhammer_eval_neg_coe_nat_of_lt 📖	mathematical	—	Polynomial.eval Ring.toSemiring NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne ascPochhammer MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	ascPochhammer_succ_eval lt_trichotomy MulZeroClass.zero_mul neg_add_cancel MulZeroClass.mul_zero
ascPochhammer_eval_neg_eq_descPochhammer 📖	mathematical	—	Polynomial.eval Ring.toSemiring NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup ascPochhammer Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne descPochhammer	—	ascPochhammer_zero descPochhammer_zero Polynomial.eval_one pow_zero mul_one ascPochhammer_succ_right mul_add Distrib.leftDistribClass Polynomial.eval_add Polynomial.eval_mul_X Nat.cast_comm Polynomial.eval_natCast_mul mul_assoc descPochhammer_succ_right mul_sub Polynomial.eval_sub pow_add pow_one neg_one_mul neg_mul_eq_mul_neg sub_eq_add_neg neg_neg
ascPochhammer_eval_one 📖	mathematical	—	Polynomial.eval AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring ascPochhammer AddMonoidWithOne.toNatCast Nat.factorial	—	Nat.cast_one ascPochhammer_nat_eq_ascFactorial Nat.one_ascFactorial
ascPochhammer_eval_succ 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Polynomial.eval Distrib.toAdd AddMonoidWithOne.toOne ascPochhammer	—	Nat.cast_one ascPochhammer_nat_eval_succ
ascPochhammer_eval_zero 📖	mathematical	—	Polynomial.eval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring ascPochhammer AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Polynomial.eval_one ascPochhammer_succ_left Polynomial.X_mul Polynomial.eval_mul_X MulZeroClass.mul_zero
ascPochhammer_eval₂ 📖	mathematical	—	Polynomial.eval ascPochhammer Polynomial.eval₂	—	ascPochhammer_map Polynomial.eval_map
ascPochhammer_map 📖	mathematical	—	Polynomial.map ascPochhammer	—	Polynomial.map_one ascPochhammer_succ_left Polynomial.map_mul Polynomial.map_X Polynomial.map_comp Polynomial.map_add
ascPochhammer_mul 📖	mathematical	—	Polynomial Polynomial.instMul ascPochhammer Polynomial.comp Polynomial.instAdd Polynomial.X Polynomial.instNatCast	—	Polynomial.one_comp mul_one add_zero ascPochhammer_succ_right Polynomial.mul_X_add_natCast_comp mul_assoc add_assoc Nat.cast_add
ascPochhammer_natDegree 📖	mathematical	—	Polynomial.natDegree ascPochhammer	—	Polynomial.natDegree_one Polynomial.natDegree_X_add_C ascPochhammer_succ_right Polynomial.natDegree_mul NeZero.one Polynomial.nontrivial Polynomial.ne_zero_of_natDegree_gt
ascPochhammer_nat_eq_ascFactorial 📖	mathematical	—	Polynomial.eval Nat.instSemiring ascPochhammer Nat.ascFactorial	—	ascPochhammer_zero Polynomial.eval_one Nat.ascFactorial_zero ascPochhammer_succ_right Polynomial.eval_mul Polynomial.eval_add Polynomial.eval_X Polynomial.eval_natCast Nat.cast_id Nat.ascFactorial_succ mul_comm
ascPochhammer_nat_eq_descFactorial 📖	mathematical	—	Polynomial.eval Nat.instSemiring ascPochhammer Nat.descFactorial	—	ascPochhammer_nat_eq_ascFactorial Nat.add_descFactorial_eq_ascFactorial'
ascPochhammer_nat_eq_natCast_ascFactorial 📖	mathematical	—	Polynomial.eval AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring ascPochhammer Nat.ascFactorial	—	ascPochhammer_nat_eq_ascFactorial
ascPochhammer_nat_eq_natCast_descFactorial 📖	mathematical	—	Polynomial.eval AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring ascPochhammer Nat.descFactorial	—	ascPochhammer_nat_eq_descFactorial
ascPochhammer_nat_eval_succ 📖	mathematical	—	Polynomial.eval Nat.instSemiring ascPochhammer	—	zero_add MulZeroClass.zero_mul ascPochhammer_eval_zero MulZeroClass.mul_zero ascPochhammer_nat_eq_ascFactorial Nat.succ_ascFactorial add_right_comm
ascPochhammer_ne_zero_eval_zero 📖	mathematical	—	Polynomial.eval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring ascPochhammer	—	ascPochhammer_eval_zero
ascPochhammer_one 📖	mathematical	—	ascPochhammer Polynomial.X	—	Polynomial.one_comp mul_one
ascPochhammer_pos 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Polynomial.eval ascPochhammer	—	Polynomial.eval_one zero_lt_one IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero ascPochhammer_succ_right mul_add Distrib.leftDistribClass Polynomial.eval_add Nat.cast_comm Polynomial.eval_natCast_mul Polynomial.eval_mul_X mul_pos IsStrictOrderedRing.toPosMulStrictMono lt_of_lt_of_le le_add_of_nonneg_right IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing Nat.cast_nonneg
ascPochhammer_succ_comp_X_add_one 📖	mathematical	—	Polynomial.comp ascPochhammer Polynomial Polynomial.instAdd Polynomial.X Polynomial.instOne Polynomial.instNSMul	—	ascPochhammer_succ_left add_mul Distrib.rightDistribClass ascPochhammer_succ_right Polynomial.mul_comp mul_comm Polynomial.add_comp Polynomial.X_comp Polynomial.natCast_comp add_comm add_assoc Mathlib.Tactic.Ring.of_eq 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_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul nsmul_eq_mul Nat.cast_add Polynomial.map_comp ascPochhammer_map Polynomial.map_add Polynomial.map_X Polynomial.map_one Polynomial.map_mul Polynomial.map_natCast
ascPochhammer_succ_eval 📖	mathematical	—	Polynomial.eval ascPochhammer Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	ascPochhammer_succ_right mul_add Distrib.leftDistribClass Polynomial.eval_add Polynomial.eval_mul_X Nat.cast_comm Polynomial.C_eq_natCast Polynomial.eval_C_mul
ascPochhammer_succ_left 📖	mathematical	—	ascPochhammer Polynomial Polynomial.instMul Polynomial.X Polynomial.comp Polynomial.instAdd Polynomial.instOne	—	ascPochhammer.eq_2
ascPochhammer_succ_right 📖	mathematical	—	ascPochhammer Polynomial Polynomial.instMul Polynomial.instAdd Polynomial.X Polynomial.instNatCast	—	zero_add ascPochhammer_one CharP.cast_eq_zero Polynomial.charP CharP.ofCharZero Nat.instCharZero add_zero one_mul ascPochhammer_succ_left Polynomial.mul_comp mul_assoc Polynomial.add_comp Polynomial.X_comp Polynomial.natCast_comp add_assoc add_comm Nat.cast_succ ascPochhammer_map Polynomial.map_mul Polynomial.map_add Polynomial.map_X Polynomial.map_natCast
ascPochhammer_zero 📖	mathematical	—	ascPochhammer Polynomial Polynomial.instOne	—	—
ascPochhammer_zero_eval_zero 📖	mathematical	—	Polynomial.eval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring ascPochhammer AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Polynomial.eval_one
descPochhammer_eq_ascPochhammer 📖	mathematical	—	descPochhammer Int.instRing Polynomial.comp Int.instSemiring ascPochhammer Polynomial Polynomial.instAdd Polynomial.instSub Polynomial.X Polynomial.instNatCast Polynomial.instOne	—	descPochhammer_zero ascPochhammer_zero Polynomial.one_comp Nat.cast_succ sub_add add_sub_cancel_right descPochhammer_succ_right ascPochhammer_succ_left Polynomial.X_mul Polynomial.mul_X_comp Polynomial.comp_assoc Polynomial.add_comp Polynomial.X_comp
descPochhammer_eval_cast 📖	mathematical	—	AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Polynomial.eval Ring.toSemiring Int.instRing descPochhammer	—	descPochhammer_map Polynomial.eval_map eq_intCast RingHom.instRingHomClass Polynomial.eval₂_at_intCast
descPochhammer_eval_coe_nat_of_lt 📖	mathematical	—	Polynomial.eval Ring.toSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne descPochhammer MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	descPochhammer_eval_eq_ascPochhammer sub_add_eq_add_sub Nat.cast_add_one neg_sub Nat.cast_sub ascPochhammer_eval_neg_coe_nat_of_lt
descPochhammer_eval_eq_ascPochhammer 📖	mathematical	—	Polynomial.eval Ring.toSemiring descPochhammer Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne AddMonoidWithOne.toOne ascPochhammer	—	descPochhammer_zero Polynomial.eval_one ascPochhammer_zero Nat.cast_succ sub_add add_sub_cancel_right descPochhammer_succ_eval ascPochhammer_succ_left Polynomial.X_mul Polynomial.eval_mul_X Polynomial.map_add Polynomial.map_X Polynomial.map_one ascPochhammer_eval_comp Polynomial.eval₂_add Polynomial.eval₂_X Polynomial.eval₂_one
descPochhammer_eval_eq_descFactorial 📖	mathematical	—	Polynomial.eval Ring.toSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne descPochhammer Nat.descFactorial	—	descPochhammer_zero Polynomial.eval_one Nat.descFactorial_zero Nat.cast_one descPochhammer_succ_right Nat.descFactorial_succ mul_sub Polynomial.eval_sub Polynomial.eval_mul_X Nat.cast_comm Polynomial.eval_natCast_mul sub_mul Nat.descFactorial_eq_zero_iff_lt Nat.cast_zero MulZeroClass.mul_zero Nat.cast_mul Nat.cast_sub
descPochhammer_eval_eq_prod_range 📖	mathematical	—	Polynomial.eval Ring.toSemiring CommRing.toRing descPochhammer Finset.prod CommRing.toCommMonoid Finset.range SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne	—	Polynomial.eval_one descPochhammer_succ_right Polynomial.eval_mul Polynomial.eval_sub Polynomial.eval_X Polynomial.eval_natCast
descPochhammer_eval_zero 📖	mathematical	—	Polynomial.eval Ring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing descPochhammer AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	Polynomial.eval_one descPochhammer_succ_left Polynomial.X_mul Polynomial.eval_mul_X MulZeroClass.mul_zero
descPochhammer_int_eq_ascFactorial 📖	mathematical	—	Polynomial.eval Ring.toSemiring Int.instRing descPochhammer Nat.ascFactorial	—	Nat.cast_add descPochhammer_eval_eq_descFactorial Nat.add_descFactorial_eq_ascFactorial
descPochhammer_map 📖	mathematical	—	Polynomial.map Ring.toSemiring descPochhammer	—	Polynomial.map_one descPochhammer_succ_left Polynomial.map_mul Polynomial.map_X Polynomial.map_comp Polynomial.map_sub
descPochhammer_mul 📖	mathematical	—	Polynomial Ring.toSemiring Polynomial.instMul descPochhammer Polynomial.comp Polynomial.instSub Polynomial.X Polynomial.instNatCast	—	Polynomial.one_comp mul_one add_zero descPochhammer_succ_right Polynomial.mul_X_sub_intCast_comp mul_assoc add_assoc Nat.cast_add sub_add_eq_sub_sub
descPochhammer_natDegree 📖	mathematical	—	Polynomial.natDegree Ring.toSemiring descPochhammer	—	Polynomial.natDegree_one Polynomial.natDegree_X_sub_C descPochhammer_succ_right Polynomial.natDegree_mul NeZero.one Polynomial.nontrivial Polynomial.ne_zero_of_natDegree_gt
descPochhammer_ne_zero_eval_zero 📖	mathematical	—	Polynomial.eval Ring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing descPochhammer	—	descPochhammer_eval_zero
descPochhammer_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne AddMonoidWithOne.toOne	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Polynomial.eval Ring.toSemiring descPochhammer	—	eq_or_lt_of_le descPochhammer_eval_eq_ascPochhammer sub_sub_cancel_left neg_add_cancel ascPochhammer_eval_zero Mathlib.Meta.Positivity.ite_nonneg_of_pos_of_nonneg Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.Positivity.nonneg_of_isNat Nat.cast_zero LT.lt.le descPochhammer_pos
descPochhammer_one 📖	mathematical	—	descPochhammer Polynomial.X Ring.toSemiring	—	Polynomial.one_comp mul_one
descPochhammer_pos 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne AddMonoidWithOne.toOne	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Polynomial.eval Ring.toSemiring descPochhammer	—	descPochhammer_eval_eq_ascPochhammer ascPochhammer_pos sub_add sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing
descPochhammer_succ_comp_X_sub_one 📖	mathematical	—	Polynomial.comp Ring.toSemiring descPochhammer Polynomial Polynomial.instSub Polynomial.X Polynomial.instOne SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Polynomial.ring DistribSMul.toSMulZeroClass instDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Polynomial.instAdd Polynomial.instNatCast	—	descPochhammer_succ_left sub_mul descPochhammer_succ_right Polynomial.mul_comp mul_comm Polynomial.sub_comp Polynomial.X_comp Polynomial.natCast_comp Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_congr Polynomial.map_comp descPochhammer_map Polynomial.map_sub Polynomial.map_X Polynomial.map_one Polynomial.map_mul Polynomial.map_add Polynomial.map_natCast
descPochhammer_succ_eval 📖	mathematical	—	Polynomial.eval Ring.toSemiring descPochhammer Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne	—	descPochhammer_succ_right mul_sub Polynomial.eval_sub Polynomial.eval_mul_X Nat.cast_comm Polynomial.C_eq_natCast Polynomial.eval_C_mul
descPochhammer_succ_left 📖	mathematical	—	descPochhammer Polynomial Ring.toSemiring Polynomial.instMul Polynomial.X Polynomial.comp Polynomial.instSub Polynomial.instOne	—	descPochhammer.eq_2
descPochhammer_succ_right 📖	mathematical	—	descPochhammer Polynomial Ring.toSemiring Polynomial.instMul Polynomial.instSub Polynomial.X Polynomial.instNatCast	—	Polynomial.one_comp mul_one CharP.cast_eq_zero Polynomial.charP CharP.ofCharZero Int.instCharZero sub_zero one_mul descPochhammer_succ_left Polynomial.mul_comp mul_assoc Polynomial.sub_comp Polynomial.X_comp Polynomial.natCast_comp Nat.cast_add Nat.cast_one sub_add_eq_sub_sub_swap descPochhammer_map Polynomial.map_mul Polynomial.map_sub Polynomial.map_X Polynomial.map_natCast
descPochhammer_zero 📖	mathematical	—	descPochhammer Polynomial Ring.toSemiring Polynomial.instOne	—	—
descPochhammer_zero_eval_zero 📖	mathematical	—	Polynomial.eval Ring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing descPochhammer AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	Polynomial.eval_one
factorial_mul_ascPochhammer 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.factorial Polynomial.eval Distrib.toAdd AddMonoidWithOne.toOne ascPochhammer	—	Nat.cast_one ascPochhammer_nat_eq_ascFactorial Nat.factorial_mul_ascFactorial
monic_ascPochhammer 📖	mathematical	—	Polynomial.Monic ascPochhammer	—	Polynomial.leadingCoeff_X_add_C ascPochhammer_succ_left Polynomial.Monic.def Polynomial.leadingCoeff_mul Polynomial.leadingCoeff_comp ne_zero_of_eq_one Polynomial.natDegree_X_add_C Polynomial.monic_X one_mul one_pow
monic_descPochhammer 📖	mathematical	—	Polynomial.Monic Ring.toSemiring descPochhammer	—	Polynomial.leadingCoeff_X_sub_C ne_zero_of_eq_one Polynomial.natDegree_X_sub_C descPochhammer_succ_left Polynomial.Monic.def Polynomial.leadingCoeff_mul Polynomial.leadingCoeff_comp Polynomial.monic_X one_mul one_pow
monotoneOn_descPochhammer_eval 📖	mathematical	—	MonotoneOn PartialOrder.toPreorder Polynomial.eval Ring.toSemiring descPochhammer Set.Ici SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne AddMonoidWithOne.toOne	—	Polynomial.eval_one CharP.cast_eq_zero CharP.ofCharZero IsStrictOrderedRing.toCharZero zero_sub LE.le.trans sub_le_self IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing zero_le_one IsStrictOrderedRing.toZeroLEOneClass add_sub_cancel_right Nat.cast_add_one Set.mem_Ici descPochhammer_succ_eval mul_le_mul IsOrderedRing.toPosMulMono IsOrderedRing.toMulPosMono sub_le_sub_right covariant_swap_add_of_covariant_add sub_nonneg_of_le descPochhammer_nonneg
pow_le_descPochhammer_eval 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne AddMonoidWithOne.toOne	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Polynomial.eval descPochhammer	—	CharP.cast_eq_zero CharP.ofCharZero IsStrictOrderedRing.toCharZero sub_zero pow_zero Polynomial.eval_one LE.le.trans sub_le_self IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing zero_le_one IsStrictOrderedRing.toZeroLEOneClass le_of_sub_nonneg covariant_swap_add_of_covariant_add sub_nonneg add_sub_cancel_right Nat.cast_add_one pow_succ descPochhammer_succ_eval sub_add mul_le_mul IsOrderedRing.toPosMulMono IsOrderedRing.toMulPosMono LE.le.trans' pow_le_pow_left₀ le_add_of_nonneg_right le_rfl descPochhammer_nonneg

---

← Back to Index