mul_dvd

Mathlib.Algebra.Divisibility.Units

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

English

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

Русский

Если IsRelPrime(x,y) и x|z и y|z, тогда x·y|z.

LaTeX

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

Lean4

theorem mul_dvd (H : IsRelPrime x y) (H1 : x ∣ z) (H2 : y ∣ z) : x * y ∣ z :=
  H.mul_dvd_of_left_isPrimal H1 H2 (DecompositionMonoid.primal x)

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

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

Разделы

Аффилиация

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