hilbertPoly_smul — Mathlib

English

HilbertPoly is homogeneous with respect to scalar multiplication: hilbertPoly(a•p, d) = a•hilbertPoly(p, d).

Русский

Хилбертов полином гомогенный по скалярам: hilbertPoly(a·p, d) = a·hilbertPoly(p, d).

LaTeX

$$$\operatorname{hilbertPoly}(a \cdot p, d) = a \cdot \operatorname{hilbertPoly}(p, d)$$$

Lean4

theorem hilbertPoly_smul (a : F) (p : F[X]) (d : ℕ) : hilbertPoly (a • p) d = a • hilbertPoly p d :=
  by
  delta hilbertPoly
  induction d with
  | zero => simp only [smul_zero]
  | succ d _ =>
    simp only
    rw [← sum_def _ fun _ r => r • _, ← sum_def _ fun _ r => r • _, Polynomial.smul_sum,
      sum_smul_index' _ _ _ fun i => zero_smul F (preHilbertPoly F d i)]
    simp only [smul_assoc]

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