mul — Mathlib

English

If x is integral over R in A, then its image in a subalgebra or submodule remains integral over R.

Русский

Если x интегрально над R в A, то его образ в подалгебре сохраняет интегральность над R.

LaTeX

$$$\text{If } x \in A \text{ is integral over }R, \text{ then its image in a substructure is integral over }R.$$$

Lean4

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

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