English
For a commutative monoid α and natural n, the nth power map n ↦ x^n is a monoid endomorphism α → α.
Русский
Для коммутативного моноида α и натурального n отображение n ↦ x^n задаёт эндоморфизм моноидов α → α.
LaTeX
$$$\\text{powMonoidHom}(n) : α \\to^* α$ with $\\text{toFun}(x) = x^n$, $\\text{map_one'} = 1^n$, $\\text{map_mul'}(a,b) = a^n b^n = (ab)^n$.$$
Lean4
/-- The `n`-th power map (for an integer `n`) on a commutative group, considered as a group
homomorphism. -/
@[to_additive (attr := simps) /-- Multiplication by an integer `n` on a commutative additive group,
considered as an additive group homomorphism. -/
]
def zpowGroupHom (n : ℤ) : α →* α where
toFun := (· ^ n)
map_one' := one_zpow n
map_mul' a b := mul_zpow a b n
