prod — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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