sum_mem — Mathlib

English

If an ideal I contains each term f(c) for c in a finite set t, then the sum over t of f(c) lies in I.

Русский

Если для каждого элемента c из конечного множества t имеет место f(c) ∈ I, то сумма ∑_{c∈t} f(c) принадлежит I.

LaTeX

$$If (∀ c ∈ t, f c ∈ I), then (∑ i ∈ t, f i) ∈ I$$

Lean4

theorem sum_mem (I : Ideal α) {ι : Type*} {t : Finset ι} {f : ι → α} : (∀ c ∈ t, f c ∈ I) → (∑ i ∈ t, f i) ∈ I :=
  Submodule.sum_mem I

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