Mathlib Map

Theorems · Theorem · commutative algebra

BinomialRing.factorial_nsmul_multichoose

∀ {R : Type u_1} {inst : AddCommMonoid R} {inst_1 : Pow R ℕ} [self : BinomialRing R] (r : R) (n : ℕ),
  n.factorial • BinomialRing.multichoose r n = (ascPochhammer ℕ n).smeval r

The nth ascending Pochhammer polynomial evaluated at any element is divisible by n!

Defined in
Mathlib.RingTheory.Binomial
Cited by
1 results in Mathlib
Foundations
Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
BinomialRing
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Ring.factorial_nsmul_multichoose_eq_ascPochhammer · cited by 12Ring.factorial_nsmul_mult…AddCommMonoid · cited by 12281AddCommMonoidNat.factorial · cited by 616Nat.factorialascPochhammer · cited by 80ascPochhammerPolynomial.smeval · cited by 65Polynomial.smevalBinomialRing · cited by 46BinomialRingBinomialRing.multichoose · cited by 2BinomialRing.multichooseBinomialRing.factorial_nsmul_…CITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.