gcd_one_right

Mathlib.Algebra.GCDMonoid.Basic

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

← MathLib Explorer

English

For a normalized gcd monoid α, gcd(a,1) = 1 for all a.

Русский

В нормализованном НОД-монойде gcd(a,1) = 1 для любого a.

LaTeX

$$$$ \gcd(a,1) = 1 $$$$

Lean4

@[simp]
theorem gcd_one_right [NormalizedGCDMonoid α] (a : α) : gcd a 1 = 1 :=
  dvd_antisymm_of_normalize_eq (normalize_gcd _ _) normalize_one (gcd_dvd_right _ _) (one_dvd _)

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

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

Разделы

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

Аффилиация

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