The units of a finite group with zero are its roots of unity

For a finite commutative group with zero F with q elements, every unit satisfies x ^ (q - 1) = 1, so the group μ_{q-1} of (q-1)-st roots of unity is all of Fˣ. This file records that identification. The main example is the multiplicative structure of a finite field.

Mathlib has the statement for the prime fields (ZMod.rootsOfUnity_eq_top); the version here is for an arbitrary finite commutative group with zero and is indexed by Nat.card.

Main results

• TauCeti.rootsOfUnity_natCard_sub_one_eq_top and TauCeti.rootsOfUnityEquivUnits: the (q-1)-st roots of unity of F are exactly its units.

theorem TauCeti.rootsOfUnity_natCard_sub_one_eq_top (F : Type u_1) [Finite F] [CommGroupWithZero F] : rootsOfUnity (Nat.card F - 1) F = ⊤

Every unit of a finite commutative group with zero with q elements is a (q-1)-st root of unity; in particular every unit of a finite field is.

noncomputable def TauCeti.rootsOfUnityEquivUnits (F : Type u_1) [Finite F] [CommGroupWithZero F] : ↥(rootsOfUnity (Nat.card F - 1) F) ≃* Fˣ

The (q-1)-st roots of unity of a finite commutative group with zero with q elements, a finite field for instance, are its units.

Equations

• TauCeti.rootsOfUnityEquivUnits F = (MulEquiv.subgroupCongr ⋯).trans Subgroup.topEquiv

@[simp]

theorem TauCeti.rootsOfUnityEquivUnits_apply (F : Type u_1) [Finite F] [CommGroupWithZero F] (ζ : ↥(rootsOfUnity (Nat.card F - 1) F)) : (rootsOfUnityEquivUnits F) ζ = ↑ζ