eq_iff_eq_on_generator — Mathlib

English

Two monoid homomorphisms are equal iff they agree on a generator g of G.

Русский

Два гомоморфизма моноидов равны тогда и только тогда, когда они совпадают на порождающем элементе g группы G.

LaTeX

$$f1 = f2 ⇔ f1(g) = f2(g)$$

Lean4

/-- Two group homomorphisms `G →* G'` are equal if and only if they agree on a generator of `G`. -/
@[to_additive /-- Two homomorphisms `G →+ G'` of additive groups are equal if and only if they agree
    on a generator of `G`. -/
    ]
theorem eq_iff_eq_on_generator (f₁ f₂ : G →* G') : f₁ = f₂ ↔ f₁ g = f₂ g :=
  by
  rw [DFunLike.ext_iff]
  refine ⟨fun H ↦ H g, fun H x ↦ ?_⟩
  obtain ⟨n, hn⟩ := mem_zpowers_iff.mp <| hg x
  rw [← hn, map_zpow, map_zpow, H]

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