mk_pow

Mathlib.GroupTheory.GroupAction.DomAct.Basic

URI: https://scilib.ai/kg/mathlib#DomMulAct.mk_pow

English

If M is a Monoid, then mk(a^{n}) = (mk a)^{n} for every a ∈ M and every natural n.

Русский

Пусть M — моноид. Тогда для любого a ∈ M и любого натурального n выполняется mk(a^{n}) = (mk a)^{n}.

LaTeX

$$$\forall a \in M, \forall n \in \mathbb{N}:\ mk(a^{n}) = (mk a)^{n}$$$

Lean4

@[to_additive (attr := simp)]
theorem mk_pow [Monoid M] (a : M) (n : ℕ) : mk (a ^ n) = mk a ^ n :=
  rfl

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

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

Разделы

Аффилиация

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