algebraMap_isIntegral_iff — Mathlib

English

The integral-ness of the structure map algebraMap R A is equivalent to A being integral over R.

Русский

Интегральность отображения алгебраMap из R в A эквивалентна тому, что A интегральна над R.

LaTeX

$$$(algebraMap R A).IsIntegral \iff \text{Algebra.IsIntegral } R A$$

Lean4

theorem algebraMap_isIntegral_iff : (algebraMap R A).IsIntegral ↔ Algebra.IsIntegral R A :=
  (Algebra.isIntegral_iff ..).symm

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