map_cyclic — Mathlib

English

If G is cyclic and σ is a monoid homomorphism from G to G, then there exists an integer m such that σ(g) = g^m for all g ∈ G.

Русский

Пусть G циклична и σ: G →* G — гомоморфизм. Тогда существует целое m, такое что для каждого g ∈ G выполнено σ(g) = g^m.

LaTeX

$$$[IsCyclic(G)](σ : G \rightarrow^* G) \Rightarrow \exists m \in \mathbb{Z}, \forall g \in G, σ(g) = g^m$$$

Lean4

@[to_additive]
theorem map_cyclic [h : IsCyclic G] (σ : G →* G) : ∃ m : ℤ, ∀ g : G, σ g = g ^ m :=
  by
  obtain ⟨h, hG⟩ := IsCyclic.exists_generator (α := G)
  obtain ⟨m, hm⟩ := hG (σ h)
  refine ⟨m, fun g => ?_⟩
  obtain ⟨n, rfl⟩ := hG g
  rw [MonoidHom.map_zpow, ← hm, ← zpow_mul, ← zpow_mul']

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