tower_bot_of_field — Mathlib

English

Let R → A → B be a tower with A a field and B a nontrivial ring. If x ∈ A is integral over R via the map A → B, then x is integral over R.

Русский

Пусть R → A → B образуют башню, где A — поле, B — ненулевая кольцо. Если x ∈ A интегрирован над R через A → B, то x интегрирован над R.

LaTeX

$$$[\\text{CommRing } R, \\text{Field } A, \\text{Ring } B] \\,\\Rightarrow \\, (x \\in A) \\rightarrow (\\text{IsIntegral}(R, x) \\\\Rightarrow \\text{IsIntegral}(R, x))$$$

Lean4

theorem tower_bot_of_field {R A B : Type*} [CommRing R] [Field A] [Ring B] [Nontrivial B] [Algebra R A] [Algebra A B]
    [Algebra R B] [IsScalarTower R A B] {x : A} (h : IsIntegral R (algebraMap A B x)) : IsIntegral R x :=
  h.tower_bot (algebraMap A B).injective

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