ofNat_nsmul_eq_mul

Mathlib.Data.Nat.Cast.Basic

URI: https://scilib.ai/kg/mathlib#Nat.ofNat_nsmul_eq_mul

English

For n ≥ 2, the OfNat embedding satisfies ofNat(n) • a = ofNat(n) · a.

Русский

При n ≥ 2 интеграция OfNat(n) • a = OfNat(n) · a.

LaTeX

$$$ \operatorname{OfNat}(n) \cdot a = \operatorname{OfNat}(n) \; a \quad (n \text{ nat}, n \ge 2)$$$

Lean4

theorem ofNat_nsmul_eq_mul (n : ℕ) [n.AtLeastTwo] (a : α) : ofNat(n) • a = ofNat(n) * a := by simp [nsmul_eq_mul]

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

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

Разделы

Аффилиация

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