image_pow_of_ne_zero — Mathlib

English

For a MulHomClass F, the image of s^n equals the nth power of the image of s when n ≠ 0.

Русский

Для отображения из класса гомоморфизмов умножения, образ множества s^n равен n-й степени образа s при n ≠ 0.

LaTeX

$$$ f '' (s^n) = (f '' s)^n \quad (n \neq 0) $$$

Lean4

@[to_additive]
theorem image_pow_of_ne_zero [MulHomClass F α β] : ∀ {n}, n ≠ 0 → ∀ (f : F) (s : Set α), f '' (s ^ n) = (f '' s) ^ n
  | 1, _ => by simp
  | n + 2, _ => by simp [image_mul, pow_succ _ n.succ, image_pow_of_ne_zero]

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