cast_div_ofNat_charZero — Mathlib

English

For natural numbers m,n with n|m, the cast of m/n from integers to a division ring k of characteristic zero equals m/n in k.

Русский

Для натуральных m,n c условием n|m, каст деления m/n из целых в кольцо деления k совпадает с m/n в k.

LaTeX

$$$\\forall m,n\\in\\mathbb{N},\\ n\\mid m\\Rightarrow (((m:\\mathbb{Z})/(n:\\mathbb{Z}):\\mathbb{Z}) : k) = m/n$$$

Lean4

@[simp, norm_cast]
theorem cast_div_ofNat_charZero {k : Type*} [DivisionRing k] [CharZero k] {m n : ℕ} (n_dvd : n ∣ m) :
    (((m : ℤ) / (n : ℤ) : ℤ) : k) = m / n := by
  rw [cast_div_charZero (Int.ofNat_dvd.mpr n_dvd), cast_natCast, cast_natCast]

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