Nat.macaulayPow
The Macaulay raising operation computed recursively from the binomial expansion.
Source context 1 command
Surrounding namespaces, section variables, and local commands at this declaration.
namespace NatLean source · full declaration
def macaulayPow : ℕ → ℕ → ℕ
| 0, _ => 0
| d + 1, a =>
(Nat.findGreatest (fun k => k.choose (d + 1) ≤ a) (a + d + 1) + 1).choose (d + 2) +
macaulayPow d (a - (Nat.findGreatest (fun k => k.choose (d + 1) ≤ a) (a + d + 1)).choose (d
+ 1))