of_mul_left_left

Mathlib.RingTheory.Coprime.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

theorem of_mul_left_left (H : IsCoprime (x * y) z) : IsCoprime x z :=
  let ⟨a, b, h⟩ := H
  ⟨a * y, b, by rwa [mul_right_comm, mul_assoc]⟩

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

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

Разделы

Аффилиация

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