of_isMaximal_liesOver

Mathlib.RingTheory.Ideal.GoingUp

URI: https://scilib.ai/kg/mathlib#Ideal.IsMaximal.of_isMaximal_liesOver

English

If P is a maximal ideal of B and P.LiesOver p, then p is maximal in A.

Русский

Если P — максимальный идеал B и P лежит над p, то p — максимальный в A.

LaTeX

$$$P.IsMaximal \rightarrow (P.LiesOver p) \Leftrightarrow p.IsMaximal$$$

Lean4

theorem of_isMaximal_liesOver [P.IsMaximal] : p.IsMaximal :=
  by
  rw [P.over_def p]
  exact isMaximal_comap_of_isIntegral_of_isMaximal P

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

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

Разделы

Аффилиация

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