mk_zpow — Mathlib

English

If M is a DivInvMonoid, then mk(a^{n}) = mk(a)^{n} for all a ∈ M and all integers n (including negative).

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem mk_zpow [DivInvMonoid M] (a : M) (n : ℤ) : mk (a ^ n) = mk a ^ n :=
  rfl

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