natCast_div — Mathlib

English

For naturals m,n (n>0) the ordinal cast of m/n equals m/n.

Русский

Для натуральных m,n (n>0) отображение m/n в ординалы равно m/n.

LaTeX

$$$ ((m / n : \mathbb{N}) : \mathrm{Ordinal}) = m / n $$$

Lean4

@[simp, norm_cast]
theorem natCast_div (m n : ℕ) : ((m / n : ℕ) : Ordinal) = m / n :=
  by
  rcases eq_or_ne n 0 with (rfl | hn)
  · simp
  · have hn' : (n : Ordinal) ≠ 0 := Nat.cast_ne_zero.2 hn
    apply le_antisymm
    · rw [le_div hn', ← natCast_mul, Nat.cast_le, mul_comm]
      apply Nat.div_mul_le_self
    · rw [div_le hn', ← add_one_eq_succ, ← Nat.cast_succ, ← natCast_mul, Nat.cast_lt, mul_comm, ←
        Nat.div_lt_iff_lt_mul (Nat.pos_of_ne_zero hn)]
      apply Nat.lt_succ_self

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