mul_dvd_mul_iff_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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