floor_div_eq_div — Mathlib

English

Natural division is the floor of field division: for m,n ∈ ℕ, ⌊(m : K) / n⌋_+ = m / n.

Русский

Натуральное деление равно полу поля деления: для m,n ∈ ℕ, ⌊(m : K)/n⌋_+ = m/n.

LaTeX

$$$$ \lfloor (m : K) / n \rfloor_+ = m / n $$$$

Lean4

/-- Natural division is the floor of field division. -/
theorem floor_div_eq_div (m n : ℕ) : ⌊(m : K) / n⌋₊ = m / n :=
  by
  convert floor_div_natCast (m : K) n
  rw [m.floor_natCast]

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