Commit 2023-09-14 15:54 c493a2c3

View on Github →

feat: descPochhammer_natDegree (#6929)

depends on: #6918

Estimated changes

Modified Mathlib/RingTheory/Polynomial/Pochhammer.lean

added theorem descPochhammer_natDegree