natCast_mul — Mathlib

English

For natural m,n, the cast of m·n equals m·n as an ordinal.

Русский

Для натуральных m,n отображение модуля даёт тот же ординал, что и произведение.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem natCast_mul (m : ℕ) : ∀ n : ℕ, ((m * n : ℕ) : Ordinal) = m * n
  | 0 => by simp
  | n + 1 => by rw [Nat.mul_succ, Nat.cast_add, natCast_mul m n, Nat.cast_succ, mul_add_one]

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