sub — Mathlib

English

If x, y ∈ A are integral over R, then any z in the subring closure of {x,y} is integral over R.

Русский

Если x, y интегральны над R в A, то любой z в замыкании по подкольцу {x,y} интегрально над R.

LaTeX

$$$IsIntegral(R,x) \land IsIntegral(R,y) \Rightarrow z \in \text{Subring.closure}(\{x,y\}) \Rightarrow IsIntegral(R,z).$$$

Lean4

nonrec theorem sub {x y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) : IsIntegral R (x - y) :=
  hx.sub (algebraMap R A) hy

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