theorem IsAlgClosed.card_rootsOfUnity (L : Type) [Field L] [CharZero L] [IsAlgClosed L] (N : ℕ) [NeZero N] : Fintype.card ↥(rootsOfUnity N L) = N

theorem PNat.coe_dvd_iff (A B : ℕ+) : ↑A ∣ ↑B ↔ A ∣ B

theorem rootsOfUnity.pow_eq_pow {a b c : ℕ} {G : Type} [Group G] {t : G} (h : t ^ a = 1) (h2 : b ≡ c [MOD a]) : t ^ b = t ^ c

theorem PNat.castHom_val_modEq {D : ℕ} {N : ℕ+} (h : D ∣ ↑N) (e : ZMod ↑N) : ((ZMod.castHom h (ZMod D)) e).val ≡ e.val [MOD D]

noncomputable def CyclotomicCharacter_aux (L : Type) [Field L] [CharZero L] [IsAlgClosed L] : (L ≃+* L) →* ZHat

The cyclotomic character

noncomputable def CyclotomicCharacterZHat (L : Type) [Field L] [CharZero L] [IsAlgClosed L] : (L ≃+* L) →* ZHatˣ