natCast_div — Mathlib

English

If a,b ∈ ℕ and b divides a, then the rational value of a/b equals a/b when viewed in ℚ.

Русский

Если a,b ∈ ℕ и b делит a, то рациональное число a/b остаётся равным a/b после отображения в ℚ.

LaTeX

$$$\\forall a,b \\in \\mathbb{N},\\ b \\mid a \\Rightarrow ((a / b : \\mathbb{N}) : \\mathbb{Q}) = a / b$$$

Lean4

theorem natCast_div (a b : ℕ) (h : b ∣ a) : ((a / b : ℕ) : ℚ) = a / b :=
  intCast_div a b (Int.ofNat_dvd.mpr h)

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