nat_gcd_helper_dvd_left

Mathlib.Tactic.NormNum.GCD

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

Lean4

theorem nat_gcd_helper_dvd_left (x y : ℕ) (h : y % x = 0) : Nat.gcd x y = x :=
  Nat.gcd_eq_left (Nat.dvd_of_mod_eq_zero h)

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

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

Разделы

Аффилиация

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