one_notMem

Mathlib.RingTheory.Ideal.Prime

URI: https://scilib.ai/kg/mathlib#Ideal.IsPrime.one_notMem

English

For any g, (g • I).IsPrime ↔ I.IsPrime.

Русский

Для любого g, (g • I).IsPrime эквивалентно I.IsPrime.

LaTeX

$$$\forall g \in M:\ (g \cdot I).IsPrime \iff I.IsPrime$$$

Lean4

theorem one_notMem {I : Ideal α} (hI : I.IsPrime) : 1 ∉ I :=
  mt (eq_top_iff_one I).2 hI.1

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

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

Разделы

Аффилиация

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