image_pow — Mathlib

English

Let f be a monoid homomorphism between monoids α and β. For any subset S ⊆ α and any natural number n, the image under f of the nth power of S equals the nth power of the image of S: f[S^n] = (f[S])^n.

Русский

Пусть f — гомоморфизм моноидов α → β. Для любого множества S ⊆ α и натурального числа n выполняется: f[S^n] = (f[S])^n.

LaTeX

$$$f[S^n] = (f[S])^n$$$

Lean4

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

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