cast_div_of_ne_zero — Mathlib

English

If q.den ≠ 0 and r.num ≠ 0 in α, then the division respects embedding: ↑(q / r) = (↑q) / (↑r).

Русский

Если q den ≠ 0 и r num ≠ 0 в α, то деление сохраняется через вложение: ↑(q / r) = ↑q / ↑r.

LaTeX

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

Lean4

@[norm_cast]
theorem cast_div_of_ne_zero (hq : (q.den : α) ≠ 0) (hr : (r.num : α) ≠ 0) : ↑(q / r) = (q / r : α) :=
  by
  rw [div_def, cast_divNat_of_ne_zero, cast_def, cast_def, div_eq_mul_inv (_ / _), inv_div,
    (Nat.commute_cast _ _).div_mul_div_comm (Nat.commute_cast _ _)]
  · push_cast
    rfl
  · push_cast
    exact mul_ne_zero hq hr

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