tsub_mul — Mathlib

English

If b c is cancellable with respect to addition, then a(b − c) = ab − ac.

Русский

Если bc допускает вычитание к сложению, то a(b − c) = ab − ac.

LaTeX

$$$AddLECancellable (bc) \Rightarrow a(b - c) = ab - ac$$$

Lean4

protected theorem tsub_mul [MulRightMono R] {a b c : R} (h : AddLECancellable (b * c)) : (a - b) * c = a * c - b * c :=
  by
  obtain (hab | hba) := total_of (· ≤ ·) a b
  · rw [tsub_eq_zero_iff_le.2 hab, zero_mul, tsub_eq_zero_iff_le.2 (mul_le_mul_right' hab c)]
  · apply h.eq_tsub_of_add_eq
    rw [← add_mul, tsub_add_cancel_of_le hba]

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