gcd_eq_left

Mathlib.Data.PNat.Prime

URI: https://scilib.ai/kg/mathlib#PNat.gcd_eq_left

English

If m divides n, then gcd(m,n) = m.

Русский

Если m делится на n, то НОД(m,n) = m.

LaTeX

$$$ m \mid n \Rightarrow gcd(m,n)=m $$$

Lean4

theorem gcd_eq_left {m n : ℕ+} : m ∣ n → m.gcd n = m :=
  by
  rw [dvd_iff]
  intro h
  apply eq
  simp only [gcd_coe]
  apply Nat.gcd_eq_left h

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

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

Разделы

Аффилиация

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