cast_div_of_ne_zero — Mathlib

English

If p.den and q.num cast to α are nonzero, then ↑(p / q) = (p / q) in α.

Русский

Если p.den и q.num приводятся в α ненулевыми, то ↑(p/q) = p/q в α.

LaTeX

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

Lean4

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

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