sub — Mathlib

English

If x and y are integral over R in an R-algebra, then x + y is integral over R; similarly for x − y.

Русский

Если x и y интегральны над R, то x + y и x − y интегральны над R.

LaTeX

$$$IsIntegral(R,x) \land IsIntegral(R,y) \Rightarrow IsIntegral(R,x+y)\quad$ и $IsIntegral(R,x) \land IsIntegral(R,y) \Rightarrow IsIntegral(R,x−y).$$$

Lean4

theorem sub {x y : S} (hx : f.IsIntegralElem x) (hy : f.IsIntegralElem y) : f.IsIntegralElem (x - y) := by
  simpa only [sub_eq_add_neg] using hx.add f (hy.neg f)

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