isIntegralElem_zero

Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

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

English

Any ring homomorphism sends 0 to an integral element.

Русский

Любой кольцевой гомоморфизм отображает нуль в интегральный элемент.

LaTeX

$$$f(0) \\text{ интегрален над } R$$$

Lean4

theorem isIntegralElem_zero : f.IsIntegralElem 0 :=
  f.map_zero ▸ f.isIntegralElem_map

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

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

Разделы

Аффилиация

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