exists_maximal_not_isPrincipal

Mathlib.RingTheory.PrincipalIdealDomain

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

← MathLib Explorer

English

There exist x,y with gcd(a,b) = a x + b y ( Bézout's lemma ).

Русский

Существуют x,y такие, что gcd(a,b) = a x + b y (лемма Безоу).

LaTeX

$$$\exists x,y \; gcd(a,b) = a x + b y$$$

Lean4

theorem exists_maximal_not_isPrincipal (hR : ¬IsPrincipalIdealRing R) : ∃ I : Ideal R, Maximal (¬·.IsPrincipal) I :=
  zorn_le₀ _ (nonPrincipals_zorn hR)

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

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

Разделы

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

Аффилиация

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