prime_generator_of_prime

Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

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

← MathLib Explorer

English

If P is prime and principal, then its generator is prime.

Русский

Если P прост и главен (принципиален), то его порождающий элемент прост.

LaTeX

$$$\text{PrimeGeneratorPrime}(P)$$$

Lean4

theorem prime_generator_of_prime {P : Ideal A} (h : Prime P) [P.IsPrincipal] : Prime (generator P) :=
  have : Ideal.IsPrime P := Ideal.isPrime_of_prime h
  prime_generator_of_isPrime _ h.ne_zero

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

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

Разделы

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

Аффилиация

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