Theorems · Theorem · commutative algebra
Polynomial.ascPochhammer_smeval_cast
∀ (R : Type u_1) [inst : Semiring R] {S : Type u_2} [inst_1 : NonAssocSemiring S] [inst_2 : Pow S ℕ]
[inst_3 : Module R S] [IsScalarTower R S S] [NatPowAssoc S] (x : S) (n : ℕ),
(ascPochhammer R n).smeval x = (ascPochhammer ℕ n).smeval x- Defined in
- Mathlib.RingTheory.Binomial
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidproof · cited by 12,281
- IsScalarTowerstatement and proof · cited by 3,896
- Polynomial.Xproof · cited by 1,639
- NonAssocSemiringstatement and proof · cited by 805
- mul_addproof · cited by 413
- nsmul_eq_mulproof · cited by 369
- Nat.cast_smul_eq_nsmulproof · cited by 110
- ascPochhammerstatement and proof · cited by 80
- Polynomial.smevalstatement and proof · cited by 65
- NatPowAssocstatement and proof · cited by 53
Cited by3
Results whose statement or proof uses this declaration.
- Ring.descPochhammer_eq_factorial_smul_chooseproof · cited by 8
- binomialSeries_eq_ordinaryHypergeometricSeriesproof · cited by 2
- Polynomial.ascPochhammer_smeval_eq_evalproof · cited by 1