isIntegral_of_surjective — Mathlib

English

If the canonical base map R → B is surjective, then B is integral over R.

Русский

Если каноническое отображение основания R → B сюръективно, то B интегральна над R.

LaTeX

$$$\text{If }\text{algebraMap } R B: R \to B \text{ is surjective, then } B \text{ is integral over } R.$$$

Lean4

theorem isIntegral_of_surjective (H : Function.Surjective (algebraMap R B)) : Algebra.IsIntegral R B :=
  .of_surjective (Algebra.ofId R B) H

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