algebraMap — Mathlib

English

If x is integral over a subring T of R, then x is integral over R.

Русский

Если x интегрален над подпольцом T внутри R, то x интегрален над R.

LaTeX

$$$\\text{IsIntegral}_T(x) \\Rightarrow \\text{IsIntegral}_R(x)$$$

Lean4

protected theorem algebraMap [Algebra A B] [IsScalarTower R A B] {x : A} (h : IsIntegral R x) :
    IsIntegral R (algebraMap A B x) := by
  rcases h with ⟨f, hf, hx⟩
  use f, hf
  rw [IsScalarTower.algebraMap_eq R A B, ← hom_eval₂, hx, RingHom.map_zero]

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