image_pow — Mathlib

English

For any MonoidHomClass f, the image of s^n under f equals the n-th power of the image of s under f, for all n.

Русский

Для любого гомоморфизма F сохранения моноидов образ s^n под f равен n-й степени образа s под f, для любого n.

LaTeX

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

Lean4

@[to_additive]
theorem image_pow [MonoidHomClass F α β] (f : F) (s : Finset α) : ∀ n, (s ^ n).image f = s.image f ^ n
  | 0 => by simp [singleton_one]
  | n + 1 => image_pow_of_ne_zero n.succ_ne_zero ..

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