isIntegralElem_map

Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

URI: https://scilib.ai/kg/mathlib#RingHom.isIntegralElem_map

English

For any ring homomorphism f: R → S, and any x ∈ R, f(x) is integral over R.

Русский

Для любого кольцевого гомоморфизма f: R → S и любого x ∈ R, образ f(x) интегрален над R.

LaTeX

$$$f\\text{IsIntegralElem}(f(x))$$$

Lean4

theorem isIntegralElem_map {x : R} : f.IsIntegralElem (f x) :=
  ⟨X - C x, monic_X_sub_C _, by simp⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru