isPrime_of_irreducible_absNorm

Mathlib.RingTheory.Ideal.Norm.AbsNorm

URI: https://scilib.ai/kg/mathlib#Ideal.isPrime_of_irreducible_absNorm

← MathLib Explorer

English

If the absolute norm of I is irreducible, then I is a prime ideal.

Русский

Если absNorm(I) ирредуцирaемое, то I является простым идеалом.

LaTeX

$$Irreducible(absNorm(I)) ⇒ I.IsPrime$$

Lean4

theorem isPrime_of_irreducible_absNorm {I : Ideal S} (hI : Irreducible (Ideal.absNorm I)) : I.IsPrime :=
  isPrime_of_prime (UniqueFactorizationMonoid.irreducible_iff_prime.mp (irreducible_of_irreducible_absNorm hI))

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

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

Разделы

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

Аффилиация

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