nsmul_eq_mul

Mathlib.Algebra.Group.Int.Defs

URI: https://scilib.ai/kg/mathlib#Int.nsmul_eq_mul

English

For all natural n and any integer a, the action of n on a via scalar multiplication equals ordinary multiplication: n • a = n a.

Русский

Для любого натурального n и целого a выполняется: n • a = n a.

LaTeX

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

Lean4

@[simp high]
protected theorem nsmul_eq_mul (n : ℕ) (a : ℤ) : n • a = n * a :=
  rfl

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

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

Разделы

Аффилиация

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