isIntegral_algebraMap_iff — Mathlib

English

For an algebra extension with injection, IsIntegral R x in A iff IsIntegral R (algebraMap A B x) in B.

Русский

Для расширения по алгебре с инъекцией IsIntegral R x в A эквивалентно IsIntegral R (algebraMap A B x) в B.

LaTeX

$$$\\text{IsIntegral}_R(x) \\iff \\text{IsIntegral}_R(\\text{algebraMap}_{A,B}(x))$$$

Lean4

theorem isIntegral_algebraMap_iff [Algebra A B] [IsScalarTower R A B] {x : A}
    (hAB : Function.Injective (algebraMap A B)) : IsIntegral R (algebraMap A B x) ↔ IsIntegral R x :=
  isIntegral_algHom_iff (IsScalarTower.toAlgHom R A B) hAB

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