isMaximal

Mathlib.RingTheory.Ideal.GoingUp

URI: https://scilib.ai/kg/mathlib#Ideal.primesOver.isMaximal

English

For any Q in primesOver p B, the underlying ideal Q.1 in B is maximal.

Русский

Для любого Q в primesOver p B соответствующий идеал Q.1 в B максимален.

LaTeX

$$∧ Q ∈ (p.primesOver B).Elem ⇒ Q.val.IsMaximal$$

Lean4

instance isMaximal : Q.1.IsMaximal :=
  Ideal.IsMaximal.of_liesOver_isMaximal Q.1 p

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

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

Разделы

Аффилиация

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