toPrimePair

Mathlib.Order.PrimeIdeal

URI: https://scilib.ai/kg/mathlib#Order.PFilter.IsPrime.toPrimePair

← MathLib Explorer

English

For a PrimePair IF, the F-component is prime: IF.F.IsPrime.

Русский

Для PrimePair IF компонент F является простым.

LaTeX

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

Lean4

/-- Create an element of type `Order.Ideal.PrimePair` from a filter satisfying the predicate
`Order.PFilter.IsPrime`. -/
def toPrimePair {F : PFilter P} (h : IsPrime F) : Ideal.PrimePair P :=
  { I := h.compl_ideal.toIdeal
    F
    isCompl_I_F := isCompl_compl.symm }

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

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

Разделы

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

Аффилиация

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