map_pow — Mathlib

English

Let G,N be groups and H a monoid hom. For f: F, and a ∈ G, and n ∈ ℕ, f(a^n) = f(a)^n.

Русский

Пусть G — группа, H — моноидный гомоморфизм, тогда для любого a ∈ G и натурального n выполнено f(a^n) = f(a)^n.

LaTeX

$$$$ \forall a \in G,\ \forall n \in \mathbb{N},\ f(a^n) = f(a)^n. $$$$

Lean4

/-- See note [hom simp lemma priority] -/
@[to_additive (attr := simp mid) (reorder := 9 10)]
theorem map_pow [Monoid G] [Monoid H] [MonoidHomClass F G H] (f : F) (a : G) : ∀ n : ℕ, f (a ^ n) = f a ^ n
  | 0 => by rw [pow_zero, pow_zero, map_one]
  | n + 1 => by rw [pow_succ, pow_succ, map_mul, map_pow f a n]

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