degree_sum_fin_lt — Mathlib

English

The degree of the finite sum ∑ i in Fin n of C(f i) X^i is less than n.

Русский

Степень конечной суммы ∑ i∈Fin n C(f i) X^i меньше n.

LaTeX

$$$ \deg\Big(\sum_{i=0}^{n-1} C(f(i)) X^{i}\Big) < n. $$$

Lean4

theorem degree_sum_fin_lt {n : ℕ} (f : Fin n → R) : degree (∑ i : Fin n, C (f i) * X ^ (i : ℕ)) < n :=
  (degree_sum_le _ _).trans_lt <|
    (Finset.sup_lt_iff <| WithBot.bot_lt_coe n).2 fun k _hk =>
      (degree_C_mul_X_pow_le _ _).trans_lt <| WithBot.coe_lt_coe.2 k.is_lt

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