add_divInt — Mathlib

English

For integers a, b, c with c ≠ 0, (a + b)/c = a/c + b/c in ℚ.

Русский

Для целых a, b, c с c ≠ 0 выполняется (a + b)/c = a/c + b/c.

LaTeX

$$$a,b,c \in \mathbb{Z}, c \neq 0 \Rightarrow \dfrac{a+b}{c} = \dfrac{a}{c} + \dfrac{b}{c}$$$

Lean4

protected theorem add_divInt (a b c : ℤ) : (a + b) /. c = a /. c + b /. c :=
  if h : c = 0 then by simp [h]
  else by
    rw [divInt_add_divInt _ _ h h, divInt_eq_divInt_iff h (Int.mul_ne_zero h h)]
    simp [Int.add_mul, Int.mul_assoc]

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