cast_mul_of_ne_zero — Mathlib

English

If p.den and q.den cast to α are nonzero, then the product p·q cast equals p·q in α.

Русский

Если p.den и q.den приводятся в α и не нули, то произведение p·q в α равно p·q в α.

LaTeX

$$$\forall p,q \in \mathbb{Q},\ (p.den : \alpha) \neq 0 \land (q.den : \alpha) \neq 0 \Rightarrow ↑(p * q) = (p * q : \alpha).$$$

Lean4

@[norm_cast]
theorem cast_mul_of_ne_zero (hp : (p.den : α) ≠ 0) (hq : (q.den : α) ≠ 0) : ↑(p * q) = (p * q : α) :=
  by
  rw [mul_eq_mkRat, cast_mkRat_of_ne_zero, cast_def, cast_def,
    (Nat.commute_cast _ _).div_mul_div_comm (Int.commute_cast _ _)]
  · push_cast
    rfl
  · push_cast
    exact mul_ne_zero hp hq

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