map_zpowers — Mathlib

English

Let f : G →* N be a group homomorphism. Then the image of the zpowers of x under f equals the zpowers of f(x): (Subgroup.zpowers x).map f = Subgroup.zpowers (f x).

Русский

Пусть f: G →* N — гомоморфизм групп. Тогда образ zpowers(x) под действием f равен zpowers(f(x)): f(⟨x⟩) = ⟨f(x)⟩.

LaTeX

$$$\operatorname{map} f (\operatorname{zpowers}(x)) = \operatorname{zpowers}(f(x))$$$

Lean4

@[to_additive (attr := simp)]
theorem map_zpowers (f : G →* N) (x : G) : (Subgroup.zpowers x).map f = Subgroup.zpowers (f x) := by
  rw [Subgroup.zpowers_eq_closure, Subgroup.zpowers_eq_closure, f.map_closure, Set.image_singleton]

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