dvd_of_lcm_left_dvd

Mathlib.Data.Nat.GCD.Basic

URI: https://scilib.ai/kg/mathlib#Nat.dvd_of_lcm_left_dvd

English

If lcm a b divides c, then b divides c.

Русский

Если lcm(a,b) делит c, тогда b делит c.

LaTeX

$$$\mathrm{lcm}(a,b) \mid c \Rightarrow b \mid c.$$$

Lean4

theorem dvd_of_lcm_left_dvd {a b c : ℕ} (h : lcm a b ∣ c) : b ∣ c :=
  (dvd_lcm_right a b).trans h

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

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

Разделы

Аффилиация

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