isUnit_gcd_of_eq_mul_gcd — Mathlib

English

If x = gcd(x,y)·x' and y = gcd(x,y)·y' with gcd(x,y) ≠ 0, then gcd(x',y') is a unit.

Русский

Если x = gcd(x,y)·x' и y = gcd(x,y)·y' с gcd(x,y) ≠ 0, то gcd(x',y') — единица.

LaTeX

$$$x = gcd(x,y) \\cdot x' \\land y = gcd(x,y) \\cdot y' \\land gcd(x,y) \\neq 0 \\Rightarrow IsUnit(gcd(x',y'))$$$

Lean4

theorem isUnit_gcd_of_eq_mul_gcd {α : Type*} [CancelCommMonoidWithZero α] [GCDMonoid α] {x y x' y' : α}
    (ex : x = gcd x y * x') (ey : y = gcd x y * y') (h : gcd x y ≠ 0) : IsUnit (gcd x' y') :=
  by
  rw [← associated_one_iff_isUnit]
  refine Associated.of_mul_left ?_ (Associated.refl <| gcd x y) h
  convert (gcd_mul_left' (gcd x y) x' y').symm using 1
  rw [← ex, ← ey, mul_one]

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