as_sum — Mathlib

English

If p is a monic polynomial, then p can be written as p = X^deg(p) + sum_{i=0}^{deg(p)-1} coeff(p,i) · X^i.

Русский

Если p — моничный полином, то он распадается как p = X^{deg(p)} + сумма от i=0 до deg(p)-1 коэффициента p(i)·X^i.

LaTeX

$$$p\text{ Monic} \Rightarrow p = X^{\deg p} + \sum_{i=0}^{\deg p - 1} (p.coeff(i)) \cdot X^{i}.$$$

Lean4

theorem as_sum (hp : p.Monic) : p = X ^ p.natDegree + ∑ i ∈ range p.natDegree, C (p.coeff i) * X ^ i :=
  by
  conv_lhs => rw [p.as_sum_range_C_mul_X_pow, sum_range_succ_comm]
  suffices C (p.coeff p.natDegree) = 1 by rw [this, one_mul]
  exact congr_arg C hp

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