sum_smul_mem — Mathlib

English

If t is finite, f: t → M, r: t → R, and f(i) ∈ p for all i ∈ t, then ∑ r(i) f(i) ∈ p.

Русский

Если t конечно, f: t → M, r: t → R и f(i) ∈ p для всех i ∈ t, то сумма ∑ r(i) f(i) ∈ p.

LaTeX

$$For all finite t, f, r with (∀ i ∈ t, f(i) ∈ p), we have ∑ i ∈ t, r(i) • f(i) ∈ p.$$

Lean4

theorem sum_smul_mem {t : Finset ι} {f : ι → M} (r : ι → R) (hyp : ∀ c ∈ t, f c ∈ p) : (∑ i ∈ t, r i • f i) ∈ p :=
  sum_mem fun i hi => smul_mem _ _ (hyp i hi)

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