map_zpow — Mathlib

English

Group homomorphisms preserve integer powers: f(g^n) = f(g)^n for g in a group and n ∈ ℤ.

Русский

Гомоморфизмы групп сохраняют целочисленные степени: f(g^n) = f(g)^n для g в группе и n ∈ ℤ.

LaTeX

$$$f(g^{n}) = f(g)^{n}$ for all $g$ in a group and $n \\in \\mathbb{Z}$.$$

Lean4

/-- Group homomorphisms preserve integer power. -/
@[to_additive /-- Additive group homomorphisms preserve integer scaling. -/
    ]
protected theorem map_zpow [Group α] [DivisionMonoid β] (f : α →* β) (g : α) (n : ℤ) : f (g ^ n) = f g ^ n :=
  map_zpow f g n

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