hilbertPoly_add_left — Mathlib

English

HilbertPoly is additive in the polynomial argument: hilbertPoly(p+q, d) = hilbertPoly(p, d) + hilbertPoly(q, d).

Русский

Хилбертов полином линейно по аргументу; сумма равна сумме отдельных полиномов.

LaTeX

$$$\operatorname{hilbertPoly}(p+q, d) = \operatorname{hilbertPoly}(p, d) + \operatorname{hilbertPoly}(q, d)$$$

Lean4

theorem hilbertPoly_add_left (p q : F[X]) (d : ℕ) : hilbertPoly (p + q) d = hilbertPoly p d + hilbertPoly q d :=
  by
  delta hilbertPoly
  induction d with
  | zero => simp only [add_zero]
  | succ d _ =>
    simp only
    rw [← sum_def _ fun _ r => r • _]
    exact sum_add_index _ _ _ (fun _ => zero_smul ..) (fun _ _ _ => add_smul ..)

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