image_pow_of_ne_zero — Mathlib

English

If n ≠ 0 and f is a multiplicative homomorphism, then (s^n).image f = (s.image f)^n for Finset s.

Русский

Пусть n ≠ 0 и f — гомоморфизм умножения. Тогда (s^n).image f = (s.image f)^n для Finset s.

LaTeX

$$$\forall n\neq 0,\; (s^n).image f = (s.image f)^n$$$

Lean4

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

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