cast_add_of_ne_zero — Mathlib

English

If the denominators of q and r are nonzero in α, then the embedding preserves addition: ↑(q + r) = (↑q) + (↑r).

Русский

Если знаменатели q и r ненулевые в α, то вложение сохраняет сложение: ↑(q + r) = (↑q) + (↑r).

LaTeX

$$$ (q + r)^{\uparrow} = (q^{\uparrow}) + (r^{\uparrow}) $$$

Lean4

@[norm_cast]
theorem cast_add_of_ne_zero (hq : (q.den : α) ≠ 0) (hr : (r.den : α) ≠ 0) : ↑(q + r) = (q + r : α) :=
  by
  rw [add_def, cast_divNat_of_ne_zero, cast_def, cast_def, mul_comm _ q.den,
    (Nat.commute_cast _ _).div_add_div (Nat.commute_cast _ _) hq hr]
  · push_cast
    rfl
  · push_cast
    exact mul_ne_zero hq hr

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