nsmul_one

Mathlib.Data.Nat.Cast.Defs

URI: https://scilib.ai/kg/mathlib#nsmul_one

← MathLib Explorer

English

For any A with AddMonoidWithOne, and any n ∈ ℕ, n multiplied by 1 equals n.

Русский

Для любого A с AddMonoidWithOne и любого n ∈ ℕ, n раз 1 равно n.

LaTeX

$$$ n \cdot 1 = n $$$

Lean4

@[simp]
theorem nsmul_one {A} [AddMonoidWithOne A] : ∀ n : ℕ, n • (1 : A) = n
  | 0 => by simp [zero_nsmul]
  | n + 1 => by simp [succ_nsmul, nsmul_one n]

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

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

Разделы

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

Аффилиация

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