smul_eq_mul

Mathlib.SetTheory.Ordinal.Arithmetic

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

← MathLib Explorer

English

For natural n, n • a = a · n for ordinals a.

Русский

Для натурального n верно n • a = a · n для ординалов a.

LaTeX

$$$\forall n \in \mathbb{N},\forall a \in \mathrm{Ordinal},\ n \cdot a = a \cdot n$$$

Lean4

theorem smul_eq_mul : ∀ (n : ℕ) (a : Ordinal), n • a = a * n
  | 0, a => by rw [zero_nsmul, Nat.cast_zero, mul_zero]
  | n + 1, a => by rw [succ_nsmul, Nat.cast_add, mul_add, Nat.cast_one, mul_one, smul_eq_mul n]

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

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

Разделы

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

Аффилиация

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