cast_mkRat_of_ne_zero — Mathlib

English

If a ∈ ℤ and b ∈ ℕ with b ≠ 0 in α, then mkRat a b cast to α equals a/b in α.

Русский

Если a ∈ ℤ и b ∈ ℕ и b ≠ 0 в α, то mkRat a b, отображённое в α, равно a/b в α.

LaTeX

$$$\forall a \in \mathbb{Z}, \forall b \in \mathbb{N},\ b \neq 0 \Rightarrow (\operatorname{mkRat} a b : \alpha) = a / b.$$$

Lean4

@[norm_cast]
theorem cast_mkRat_of_ne_zero (a : ℤ) {b : ℕ} (hb : (b : α) ≠ 0) : (mkRat a b : α) = a / b := by
  rw [Rat.mkRat_eq_divInt, cast_divInt_of_ne_zero, Int.cast_natCast]; rwa [Int.cast_natCast]

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