of_add_mul_left_left — Mathlib

English

IsRelPrime is defined by the property that if d divides both arguments then d is a unit; the lemma shows the stability under + and * left-left.

Русский

IsRelPrime задается свойством: если d делит оба аргумента, то d единица; лемма сохраняет свойство при операциях сложения и умножения слева.

LaTeX

$$$\operatorname{IsRelPrime}(x + y \cdot z, y) \Rightarrow \operatorname{IsRelPrime}(x,y)$$$

Lean4

theorem of_add_mul_left_left (h : IsRelPrime (x + y * z) y) : IsRelPrime x y := fun _ hx hy ↦
  h (dvd_add hx <| dvd_mul_of_dvd_left hy z) hy

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