mul_dvd_mul_iff_left — Mathlib

English

In a CancelMonoidWithZero, for a ≠ 0, a b divides a c if and only if b divides c.

Русский

В CancelMonoidWithZero для a ≠ 0 верно: a b | a c ⇔ b | c.

LaTeX

$$a \neq 0 \Rightarrow (a b \mid a c \iff b \mid c)$$

Lean4

/-- Given two elements `b`, `c` of a `CancelMonoidWithZero` and a nonzero element `a`,
`a*b` divides `a*c` iff `b` divides `c`. -/
theorem mul_dvd_mul_iff_left [CancelMonoidWithZero α] {a b c : α} (ha : a ≠ 0) : a * b ∣ a * c ↔ b ∣ c :=
  exists_congr fun d => by rw [mul_assoc, mul_right_inj' ha]

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