isCoprime_mul_unit_left_left — Mathlib

English

If x is a unit, then IsCoprime (x y) z is equivalent to IsCoprime y z.

Русский

Если x является единицей, то IsCoprime (x y) z эквивалентно IsCoprime y z.

LaTeX

$$$(\text{IsUnit } x) \Rightarrow (\operatorname{IsCoprime}(x y, z) \iff \operatorname{IsCoprime}(y, z))$$$

Lean4

theorem isCoprime_mul_unit_left_left (hu : IsUnit x) (y z : R) : IsCoprime (x * y) z ↔ IsCoprime y z :=
  let ⟨u, hu⟩ := hu
  hu ▸ isCoprime_group_smul_left u y z

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