nonemptyGCDMonoid

Mathlib.RingTheory.PrincipalIdealDomain

URI: https://scilib.ai/kg/mathlib#IsBezout.nonemptyGCDMonoid

English

A Bézout domain that is a domain has a gcd operation; i.e., there exists a GCDMonoid structure on R.

Русский

Пусть R — кольцо Безу и область. Тогда существует операция НОД, т.е. существует структура GCDMonoid R.

LaTeX

$$$\\\\exists GCDMonoid(R)$$$

Lean4

instance nonemptyGCDMonoid [IsBezout R] [IsDomain R] : Nonempty (GCDMonoid R) := by classical exact ⟨toGCDDomain R⟩

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

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

Разделы

Аффилиация

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