instNonemptyNormalizedGCDMonoid

Mathlib.Algebra.GCDMonoid.Basic

URI: https://scilib.ai/kg/mathlib#instNonemptyNormalizedGCDMonoid

English

There exists a normalized gcd-monoid structure on α, i.e., there exists a NormalizedGCDMonoid on α.

Русский

Существует нормализованный gcd-монойд на α, то есть существует NormalizedGCDMonoid(α).

LaTeX

$$$$ \\exists \\mathcal{NG} : \\text{NormalizedGCDMonoid}(\\alpha). $$$$

Lean4

instance [NormalizedGCDMonoid α] : Nonempty (NormalizedGCDMonoid α) :=
  ⟨‹_›⟩

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

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

Разделы

Аффилиация

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