dvd_mul_sub_mul_mul_right_of_dvd — Mathlib

English

If p ∣ a x + b y and p ∣ c x + d y in a commutative ring, then p ∣ (a d − b c) y.

Русский

Пусть в коммутативном кольце выполняются p | a x + b y и p | c x + d y; тогда p | (a d − b c) y.

LaTeX

$$p ∣ a x + b y ∧ p ∣ c x + d y ⇒ p ∣ (a d - b c) y$$

Lean4

theorem dvd_mul_sub_mul_mul_right_of_dvd {p a b c d x y : R} (h1 : p ∣ a * x + b * y) (h2 : p ∣ c * x + d * y) :
    p ∣ (a * d - b * c) * y :=
  (mul_comm a _ ▸ mul_comm c _ ▸ dvd_mul_sub_mul_mul_left_of_dvd (add_comm (c * x) _ ▸ h2) (add_comm (a * x) _ ▸ h1))

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