I_isPrime

Mathlib.Order.PrimeIdeal

URI: https://scilib.ai/kg/mathlib#Order.Ideal.PrimePair.I_isPrime

← MathLib Explorer

English

If IF is a PrimePair, then the I-component is a prime ideal: IF.I.IsPrime.

Русский

Если IF является PrimePair, то I-компонента является простым идеалом: IF.IIsPrime.

LaTeX

$$$\\text{IF.I is prime}$.$$

Lean4

theorem I_isPrime (IF : PrimePair P) : IsPrime IF.I :=
  { IF.I_isProper with
    compl_filter := by
      rw [IF.compl_I_eq_F]
      exact IF.F.isPFilter }

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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