map_zpow' — Mathlib

English

For DivInvMonoid M,N, if f preserves inverses (f(x^{-1})=(f(x))^{-1}), then f preserves Z-powers: f(a^n) = f(a)^n for all integers n.

Русский

Для DivInvMonoid M,N, если сохраняется обратность, то сохраняются целочисленные степени: f(a^n)=f(a)^n для всех целых n.

LaTeX

$$$f(a^n) = f(a)^n \\quad \\text{for all } n \\in \\mathbb{Z}$$$

Lean4

@[to_additive]
protected theorem map_zpow' [DivInvMonoid M] [DivInvMonoid N] (f : M →* N) (hf : ∀ x, f x⁻¹ = (f x)⁻¹) (a : M) (n : ℤ) :
    f (a ^ n) = f a ^ n :=
  map_zpow' f hf a n

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