add — Mathlib

English

If x and y are integral over R in an R-algebra A, then any element adjoined from x and y is integral over R.

Русский

Если x,y интегральны над R в алгебре A, то любой элемент, получаемый при присоединении x и y, интегральен над R.

LaTeX

$$$IsIntegral(R,x) \wedge IsIntegral(R,y) \Rightarrow IsIntegral(R, \text{adjoin}(R\{x,y\})).$$$

Lean4

theorem add (f : R →+* S) {x y : S} (hx : f.IsIntegralElem x) (hy : f.IsIntegralElem y) : f.IsIntegralElem (x + y) :=
  hx.of_mem_closure f hy <|
    Subring.add_mem _ (Subring.subset_closure (Or.inl rfl)) (Subring.subset_closure (Or.inr rfl))

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