natCast_mod_omega0

Mathlib.SetTheory.Ordinal.Arithmetic

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

English

For every natural n, n mod ω equals n.

Русский

Для каждого натурального n остаток от деления n на ω равен n.

LaTeX

$$$n \bmod \omega = n$$$

Lean4

@[simp]
theorem natCast_mod_omega0 (n : ℕ) : n % ω = n :=
  mod_eq_of_lt (nat_lt_omega0 n)

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

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

Разделы

Аффилиация

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