of_mem_closure'' — Mathlib

English

If all elements of a set G are integral, then all elements of the subring closure of G are integral.

Русский

Если все элементы множества G интегральны, то все элементы замыкания подкольца G также интегральны.

LaTeX

$$$\forall x \in G, f.IsIntegralElem x \Rightarrow \forall x \in \operatorname{Subring.closure} G, f.IsIntegralElem x$$$

Lean4

theorem of_mem_closure'' {S : Type*} [CommRing S] {f : R →+* S} (G : Set S) (hG : ∀ x ∈ G, f.IsIntegralElem x) :
    ∀ x ∈ Subring.closure G, f.IsIntegralElem x := fun x hx => @IsIntegral.of_mem_closure' R S _ _ f.toAlgebra G hG x hx

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