ofFn_eq_sum_monomial — Mathlib

English

The polynomial ofFn n v equals the finite sum of monomials: ofFn n v = ∑ i : Fin n, monomial i (v i).

Русский

Многочлен ofFn n v равен конечной сумме мономиалов: ofFn n v = ∑ i : Fin n, monomial i (v i).

LaTeX

$$$\operatorname{ofFn}(n)\, v = \sum_{i : \mathrm{Fin}(n)} \operatorname{monomial}(i)\big(v(i)\big).$$$

Lean4

theorem ofFn_eq_sum_monomial {n : ℕ} (v : Fin n → R) : ofFn n v = ∑ i : Fin n, monomial i (v i) :=
  by
  by_cases h : n = 0
  · subst h
    simp [ofFn]
  · rw [as_sum_range' (ofFn n v) n <| ofFn_natDegree_lt (Nat.one_le_iff_ne_zero.mpr h) v]
    simp [Finset.sum_range]

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