sub_mul — Mathlib

English

If 0 < c and c < b and a ≠ ∞, then (a − b) * c = a * c − b * c.

Русский

Если 0 < c и c < b и a ≠ ∞, то (a − b)·c = a·c − b·c.

LaTeX

$$$ (0 < c) \land (c < b) \land (a \neq \infty) \Rightarrow (a - b) c = a c - b c $$$

Lean4

protected theorem sub_mul (h : 0 < b → b < a → c ≠ ∞) : (a - b) * c = a * c - b * c :=
  by
  rcases le_or_gt a b with hab | hab; · simp [hab, mul_left_mono hab, tsub_eq_zero_of_le]
  rcases eq_or_lt_of_le (zero_le b) with (rfl | hb); · simp
  exact (cancel_of_ne <| mul_ne_top hab.ne_top (h hb hab)).tsub_mul

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