English
If every element of a finite type α lies in zpowers a, then for every x ∈ α there exists a unique n ∈ ZMod(card α) such that x = a^n.
Русский
Пусть каждый элемент α лежит в zpowers a; тогда для каждого x ∈ α существует единственный n ∈ ZMod(card α) такой, что x = a^n.
LaTeX
$$$\exists! n : \mathbb{Z}/(\lvert \alpha \rvert)\mathbb{Z},\ x = a^{n}$$$
Lean4
@[to_additive]
theorem unique_zpow_zmod (ha : ∀ x : α, x ∈ zpowers a) (x : α) : ∃! n : ZMod (Fintype.card α), x = a ^ n.val :=
by
obtain ⟨n, rfl⟩ := ha x
refine ⟨n, (?_ : a ^ n = _), fun y (hy : a ^ n = _) ↦ ?_⟩
·
rw [← zpow_natCast, zpow_eq_zpow_iff_modEq, orderOf_eq_card_of_forall_mem_zpowers ha, Int.modEq_comm,
Int.modEq_iff_add_fac, Nat.card_eq_fintype_card, ← ZMod.intCast_eq_iff]
· rw [← zpow_natCast, zpow_eq_zpow_iff_modEq, orderOf_eq_card_of_forall_mem_zpowers ha, Nat.card_eq_fintype_card, ←
ZMod.intCast_eq_intCast_iff] at hy
simp [hy]
