nsmul_mk

Mathlib.GroupTheory.DivisibleHull

URI: https://scilib.ai/kg/mathlib#DivisibleHull.nsmul_mk

← MathLib Explorer

English

For a natural number a and m ∈ M and s ∈ ℕ+, a • mk m s = mk (a • m) s.

Русский

Для натурального a и элементов m ∈ M, s ∈ ℕ+, выполняется a • mk m s = mk (a • m) s.

LaTeX

$$$a \cdot \text{mk } m s = \text{mk } (a \cdot m) s$$$

Lean4

theorem nsmul_mk (a : ℕ) (m : M) (s : ℕ+) : a • mk m s = mk (a • m) s := by
  induction a with
  | zero => simp
  | succ n h => simp [add_nsmul, mk_add_mk_left, h]

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

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

Разделы

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

Аффилиация

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