dvd_of_dvd_mul_left

Mathlib.Algebra.Divisibility.Units

URI: https://scilib.ai/kg/mathlib#IsRelPrime.dvd_of_dvd_mul_left

English

If IsRelPrime x y and x divides y·z, then x divides z.

Русский

Если IsRelPrime x y и x делит y·z, то x делит z.

LaTeX

$$$\text{IsRelPrime}(x,y) \rightarrow x \mid (y \cdot z) \rightarrow x \mid z$$

Lean4

theorem dvd_of_dvd_mul_left (H1 : IsRelPrime x y) (H2 : x ∣ y * z) : x ∣ z :=
  H1.dvd_of_dvd_mul_right (mul_comm y z ▸ H2)

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

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

Разделы

Аффилиация

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