natCast_mod

Mathlib.SetTheory.Ordinal.Arithmetic

URI: https://scilib.ai/kg/mathlib#Ordinal.natCast_mod

← MathLib Explorer

English

For naturals m,n, ((m % n) : Ordinal) = m % n.

Русский

Для натуральных m,n, остаток m % n в ординалах равен m % n.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem natCast_mod (m n : ℕ) : ((m % n : ℕ) : Ordinal) = m % n := by
  rw [← add_left_cancel_iff, div_add_mod, ← natCast_div, ← natCast_mul, ← Nat.cast_add, Nat.div_add_mod]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru