mul_div_mul_cancel — Mathlib

English

If a ≠ 0 and c divides b, then a·b/(a·c) = b/c.

Русский

Если a ≠ 0 и c делит b, то a·b/(a·c) = b/c.

LaTeX

$$$a \neq 0 \rightarrow (c \mid b) \Rightarrow \dfrac{a \cdot b}{a \cdot c} = \dfrac{b}{c}$$$

Lean4

theorem mul_div_mul_cancel {a b c : R} (ha : a ≠ 0) (hcb : c ∣ b) : a * b / (a * c) = b / c :=
  by
  by_cases hc : c = 0; · simp [hc]
  refine eq_div_of_mul_eq_right hc (mul_left_cancel₀ ha ?_)
  rw [← mul_assoc, ← mul_div_assoc _ (by gcongr), mul_div_cancel_left₀ _ (mul_ne_zero ha hc)]

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