lcm_dvd_iff

Mathlib.Algebra.EuclideanDomain.Basic

URI: https://scilib.ai/kg/mathlib#EuclideanDomain.lcm_dvd_iff

← MathLib Explorer

English

lcm(x,y) divides z if and only if x divides z and y divides z.

Русский

lcm(x,y) делит z тогда и только тогда, когда x делит z и y делит z.

LaTeX

$$$\operatorname{lcm}(x,y) \mid z \\iff (x \mid z) \land (y \mid z)$$$

Lean4

@[simp]
theorem lcm_dvd_iff {x y z : R} : lcm x y ∣ z ↔ x ∣ z ∧ y ∣ z :=
  ⟨fun hz => ⟨(dvd_lcm_left _ _).trans hz, (dvd_lcm_right _ _).trans hz⟩, fun ⟨hxz, hyz⟩ => lcm_dvd hxz hyz⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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