of_mem_closure — Mathlib

English

If x,y,z ∈ A with hx, hy integral over R and z in the subring generated by x and y, then z is integral over R.

Русский

Пусть x,y ∈ A интегральны над R и z лежит в подкольце, порождаемом x,y; тогда z интегрален над R.

LaTeX

$$$\forall x,y,z\in A:\; (IsIntegral(R,x)\wedge IsIntegral(R,y)\wedge z\in\langle x,y\rangle)\Rightarrow IsIntegral(R,z).$$$

Lean4

nonrec theorem of_mem_closure {x y z : A} (hx : IsIntegral R x) (hy : IsIntegral R y)
    (hz : z ∈ Subring.closure ({ x, y } : Set A)) : IsIntegral R z :=
  hx.of_mem_closure (algebraMap R A) hy hz

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