instIsPrimeSupport

Mathlib.Algebra.Order.Ring.Ordering.Basic

URI: https://scilib.ai/kg/mathlib#RingPreordering.instIsPrimeSupport

English

The RingPreordering support is a prime ideal.

Русский

Опора RingPreordering является простым идеалом.

LaTeX

$$$P.support.IsPrime$$$

Lean4

instance : P.support.IsPrime := by simpa using Ideal.bot_prime

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

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

Разделы

Аффилиация

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