nat_gcd_helper_dvd_right

Mathlib.Tactic.NormNum.GCD

URI: https://scilib.ai/kg/mathlib#Tactic.NormNum.nat_gcd_helper_dvd_right

Lean4

theorem nat_gcd_helper_dvd_right (x y : ℕ) (h : x % y = 0) : Nat.gcd x y = y :=
  Nat.gcd_eq_right (Nat.dvd_of_mod_eq_zero h)

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

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

Разделы

Аффилиация

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