English
In a finite cyclic group G with card d, if t^a = t^b for all t, then a = b in ZMod d.
Русский
В конечной циклической группе G с порядком d, если t^a = t^b для всех t, то a = b в ZMod d.
LaTeX
$$For a finite group G with card d and a,b ∈ ZMod d, if ∀ t ∈ G, t^a = t^b, then a = b.$$
Lean4
@[to_additive]
theorem ext [Finite G] [IsCyclic G] {d : ℕ} {a b : ZMod d} (hGcard : Nat.card G = d)
(h : ∀ t : G, t ^ a.val = t ^ b.val) : a = b :=
by
have : NeZero (Nat.card G) := ⟨Nat.card_pos.ne'⟩
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := G)
specialize h g
subst hGcard
rw [pow_eq_pow_iff_modEq, orderOf_eq_card_of_forall_mem_zpowers hg, ← ZMod.natCast_eq_natCast_iff] at h
simpa [ZMod.natCast_val, ZMod.cast_id'] using h
