cast_sub_of_ne_zero — Mathlib

English

If p.den and q.den cast to α are nonzero, then ↑(p − q) = (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_sub_of_ne_zero (hp : (p.den : α) ≠ 0) (hq : (q.den : α) ≠ 0) : ↑(p - q) = (p - q : α) := by
  simp [sub_eq_add_neg, cast_add_of_ne_zero, hp, hq]

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