cast_mul_of_ne_zero — Mathlib

English

If q and r have nonzero denominators in α, then ↑(q · r) = ↑q · ↑r.

Русский

Если знаменатели q и r ненулевые в α, то ↑(q · r) = ↑q · ↑r.

LaTeX

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

Lean4

@[norm_cast]
theorem cast_mul_of_ne_zero (hq : (q.den : α) ≠ 0) (hr : (r.den : α) ≠ 0) : ↑(q * r) = (q * r : α) :=
  by
  rw [mul_def, cast_divNat_of_ne_zero, cast_def, cast_def,
    (Nat.commute_cast _ _).div_mul_div_comm (Nat.commute_cast _ _)]
  · push_cast
    rfl
  · push_cast
    exact mul_ne_zero hq hr

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