theorem FiniteFields.finite_field_units_cyclic (F : Type u_1) [Field F] (G : Subgroup Fˣ) [Finite ↥G] : IsCyclic ↥G

theorem FiniteFields.finite_field_existence_uniqueness (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) (hn : n ≠ 0) : Nat.card (GaloisField p n) = p ^ n ∧ ∀ (K : Type u_1) [inst : Field K] [inst_1 : Algebra (ZMod p) K], Nat.card K = p ^ n → Nonempty (K ≃ₐ[ZMod p] GaloisField p n)

theorem FiniteFields.finite_field_simple_extension_and_irreducibles (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) (hn : 0 < n) : (∃ (α : GaloisField p n), (ZMod p)⟮α⟯ = ⊤) ∧ ∃ (f : Polynomial (ZMod p)), Irreducible f ∧ f.natDegree = n