of_mul_right_right

Mathlib.RingTheory.Coprime.Basic

URI: https://scilib.ai/kg/mathlib#IsCoprime.of_mul_right_right

English

If IsCoprime x (y z) then IsCoprime x z.

Русский

Если IsCoprime x (y z), то IsCoprime x z.

LaTeX

$$$IsCoprime(x, y\cdot z) \Rightarrow IsCoprime(x,z)$$$

Lean4

theorem of_mul_right_right (H : IsCoprime x (y * z)) : IsCoprime x z :=
  by
  rw [mul_comm] at H
  exact H.of_mul_right_left

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

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

Разделы

Аффилиация

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