isAlgebraic_algebraMap_iff — Mathlib

English

For an injective algebra map, IsAlgebraic(R, algebraMap S A a) iff IsAlgebraic(R, a).

Русский

Для инъективного алгебраистического отображения IsAlgebraic(R, algebraMap S A a) эквивалентно IsAlgebraic(R, a).

LaTeX

$$$\text{Injective}(algebraMap S A) \Rightarrow IsAlgebraic(R, algebraMap S A(a)) \iff IsAlgebraic(R, a)$$$

Lean4

theorem isAlgebraic_algebraMap_iff {a : S} (h : Function.Injective (algebraMap S A)) :
    IsAlgebraic R (algebraMap S A a) ↔ IsAlgebraic R a :=
  isAlgebraic_algHom_iff (IsScalarTower.toAlgHom R S A) h

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