natCast_mul_omega0

Mathlib.SetTheory.Ordinal.Principal

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

English

If n is a positive natural, then n * ω = ω.

Русский

Если n — положительное натуральное, то n * ω = ω.

LaTeX

$$$\forall n \in \mathbb{N}, n > 0 \Rightarrow n * \omega = \omega.$$$

Lean4

theorem natCast_mul_omega0 {n : ℕ} (hn : 0 < n) : n * ω = ω :=
  mul_omega0 (mod_cast hn) (nat_lt_omega0 n)

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

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

Разделы

Аффилиация

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