mul_add_div — Mathlib

English

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

Русский

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

LaTeX

$$$b \\\\\\neq 0 \\\\Rightarrow \\\\frac{b \\\\\\cdot a + c}{b} = a + \\frac{c}{b}$$$

Lean4

theorem mul_add_div (a) {b : Ordinal} (b0 : b ≠ 0) (c) : (b * a + c) / b = a + c / b :=
  by
  apply le_antisymm
  · apply (div_le b0).2
    rw [mul_succ, mul_add, add_assoc, add_lt_add_iff_left]
    apply lt_mul_div_add _ b0
  · rw [le_div b0, mul_add, add_le_add_iff_left]
    apply mul_div_le

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