isMaximal

Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

URI: https://scilib.ai/kg/mathlib#IsDedekindDomain.HeightOneSpectrum.isMaximal

English

Let R be a Dedekind domain and v a height-one prime in R. Then the corresponding ideal v.asIdeal is a maximal ideal.

Русский

Пусть R — кольцо Дедекинда, и v — идеал высоты 1. Соответствующий ему идеал v.asIdeal является максимальным.

LaTeX

$$$\\mathrm{IsMaximal}(v.asIdeal)$$$

Lean4

instance isMaximal : v.asIdeal.IsMaximal :=
  v.isPrime.isMaximal v.ne_bot

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

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

Разделы

Аффилиация

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