English
Two multiplicative characters on a monoid with cyclic unit group are equal iff they take equal values on a generator g.
Русский
Два мультипликативных симвлa на моноиде с циклической единичной группой равны тогда и только тогда, когда они принимают одинаковые значения на генераторе g.
LaTeX
$$χ1 = χ2 ↔ χ1(g) = χ2(g)$$
Lean4
/-- Two multiplicative characters on a monoid whose unit group is generated by `g`
are equal if and only if they agree on `g`. -/
theorem eq_iff {R R' : Type*} [CommMonoid R] [CommMonoidWithZero R'] {g : Rˣ} (hg : ∀ x, x ∈ Subgroup.zpowers g)
(χ₁ χ₂ : MulChar R R') : χ₁ = χ₂ ↔ χ₁ g.val = χ₂ g.val := by
rw [← Equiv.apply_eq_iff_eq equivToUnitHom, MonoidHom.eq_iff_eq_on_generator hg, ← coe_equivToUnitHom, ←
coe_equivToUnitHom, Units.ext_iff]
