Revision #3638 → #4187 · back to history
modifiedStirling number formula8112746bba3a
| Field | From #3638 | To #4187 |
|---|
| mathlib.decl | — | Nat.stirlingFirst |
| mathlib.match_kind | — | invocation |
| mathlib.module | — | Mathlib.Combinatorics.Enumerative.Stirling |
| note | Unsigned Stirling numbers of the first kind and the ₃F₂ representation are not formalized in Mathlib under a verified name; flagging the prior `Nat.stirlingFirst` reference as unverified. | Unsigned Stirling numbers of the first kind exist in Mathlib as `Nat.stirlingFirst` (verified), but the ₃F₂ formula representation is not formalized. |
| status | not_formalized | partial |
modifiedRational functionf73805191d61
| Field | From #3638 | To #4187 |
|---|
| mathlib.module | Mathlib.FieldTheory.RatFunc.Basic | Mathlib.FieldTheory.RatFunc.Defs |
| note | Rational functions over a field are formalized as `RatFunc`. | Rational functions over a field are formalized as `RatFunc` (module `Mathlib.FieldTheory.RatFunc.Defs`). |
addedQ-analogb59569de794e
addedAsymptotic expansion44c9a7a91f8a
addedWell-poised seriesf967dde409f8
addedKummer's second formula (b=2a case)060bb628bbd1
addedGeneral solution of hypergeometric ODE (2F1)91ba5a5e46fd
addedPolylogarithma590577f0dc9
addedSemi-simple Lie groupaa0547270f11