mul — Mathlib

English

If x and y are integral over R in an R-algebra, then x + y and x*y are integral over R.

Русский

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

LaTeX

$$$IsIntegral(R,x) \land IsIntegral(R,y) \Rightarrow IsIntegral(R,x+y) \land IsIntegral(R,x\cdot y).$$$

Lean4

theorem mul {x y : S} (hx : f.IsIntegralElem x) (hy : f.IsIntegralElem y) : f.IsIntegralElem (x * y) :=
  hx.of_mem_closure f hy (Subring.mul_mem _ (Subring.subset_closure (Or.inl rfl)) (Subring.subset_closure (Or.inr rfl)))

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