sum — Mathlib

English

If a finite family of elements f(x) are all integral over R, then their finite sum is integral over R.

Русский

Если конечное семейство элементов интегрально над R, их сумма интегральна над R.

LaTeX

$$$(\forall x \in s, IsIntegral R (f x)) \Rightarrow IsIntegral R (\sum x \in s, f x)$$$

Lean4

theorem sum {α : Type*} {s : Finset α} (f : α → A) (h : ∀ x ∈ s, IsIntegral R (f x)) : IsIntegral R (∑ x ∈ s, f x) :=
  (integralClosure R A).sum_mem h

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