dvd_mul_sub_mul — Mathlib

English

In any nonunital commutative ring, if k divides a − b and k divides x − y, then k divides a x − b y.

Русский

В любом неединичном коммутативном кольце, если k делится на a − b и k делится на x − y, то k делится на a x − b y.

LaTeX

$$$k \mid a - b \land k \mid x - y \Rightarrow k \mid a x - b y$$$

Lean4

theorem dvd_mul_sub_mul {k a b x y : α} (hab : k ∣ a - b) (hxy : k ∣ x - y) : k ∣ a * x - b * y :=
  by
  convert dvd_add (hxy.mul_left a) (hab.mul_right y) using 1
  rw [mul_sub_left_distrib, mul_sub_right_distrib]
  simp only [sub_eq_add_neg, add_assoc, neg_add_cancel_left]

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