hilbertPoly_mul_one_sub_pow_add — Mathlib

English

For p ∈ F[X] and d,e ∈ ℕ, hilbertPoly(p*(1 - X)^e, d+e) = hilbertPoly(p, d).

Русский

Для любого p и d,e: хилбертов полином от p*(1 - X)^e на d+e равен хилбертовому полиному от p на d.

LaTeX

$$$\operatorname{hilbertPoly}(p \cdot (1 - X)^e, d + e) = \operatorname{hilbertPoly}(p, d)$$$

Lean4

theorem hilbertPoly_mul_one_sub_pow_add (p : F[X]) (d e : ℕ) :
    hilbertPoly (p * (1 - X) ^ e) (d + e) = hilbertPoly p d := by
  induction e with
  | zero => simp
  | succ e he => rw [pow_add, pow_one, ← mul_assoc, ← add_assoc, hilbertPoly_mul_one_sub_succ, he]

Похожие утверждения