tower_bot_of_injective — Mathlib

English

If A is algebraic over R and the map S → A is injective, then S is algebraic over R.

Русский

Если A алгебраичен над R и отображение S → A инъективно, то S алгебраичен над R.

LaTeX

$$$\mathrm{Algebra.IsAlgebraic}\ R\ A \rightarrow (\mathrm{Injective}(\mathrm{algebraMap}\ S\ A)) \Rightarrow \mathrm{Algebra.IsAlgebraic}\ R\ S$$$

Lean4

theorem tower_bot_of_injective [Algebra.IsAlgebraic R A] (hinj : Function.Injective (algebraMap S A)) :
    Algebra.IsAlgebraic R S where
  isAlgebraic x := by simpa [isAlgebraic_algebraMap_iff hinj] using isAlgebraic (R := R) (A := A) (algebraMap _ _ x)

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