degree_eq_sum — Mathlib

English

Let σ be finite and f : σ →₀ R be a finitely supported function. Then the degree of f equals the sum of its values: deg f = ∑_{i ∈ σ} f(i).

Русский

Пусть σ конечно, и f : σ →₀ R — конечно поддерживаемая функция. Тогда степень f равна сумме её коэффициентов: deg f = ∑_{i ∈ σ} f(i).

LaTeX

$$$\deg f = \sum_{i \in \sigma} f(i)$$$

Lean4

theorem degree_eq_sum [Fintype σ] (f : σ →₀ R) : f.degree = ∑ i, f i := by rw [degree, Finset.sum_subset] <;> simp

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