gcd_one_left

Mathlib.Algebra.GCDMonoid.Basic

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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