gcd_eq_right_iff_dvd

Mathlib.Data.PNat.Prime

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

English

Let m,n be positive integers. Then gcd(n,m)=m iff m divides n.

Русский

Пусть m,n > 0. Тогда gcd(n,m)=m эквивалентно m делится на n.

LaTeX

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

Lean4

theorem gcd_eq_right_iff_dvd {m n : ℕ+} : n.gcd m = m ↔ m ∣ n :=
  by
  rw [gcd_comm]
  apply gcd_eq_left_iff_dvd

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

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

Разделы

Аффилиация

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