Results on intermediate fields of finite fields

def FiniteField.intermediateField (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Finite L] [Algebra K L] (n : ℕ) : IntermediateField K L

For each n, {x : L | x ^ q ^ n = x} is an intermediate field (where q = Nat.card K).

theorem FiniteField.mem_intermediateField_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Finite L] [Algebra K L] {n : ℕ} {x : L} : x ∈ intermediateField K L n ↔ x ^ Nat.card K ^ n = x

theorem FiniteField.intermediateField_eq_rootSet {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Finite L] [Algebra K L] {n : ℕ} (hn : n ≠ 0) : ↑(intermediateField K L n) = (Polynomial.X ^ Nat.card K ^ n - Polynomial.X).rootSet L

theorem FiniteField.mem_intermediateField_iff' {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Finite L] [Algebra K L] {n : ℕ} {x : L} : x ∈ intermediateField K L n ↔ x = 0 ∨ x ^ (Nat.card K ^ n - 1) = 1

theorem FiniteField.intermediateField_eq_insert_zero_nthRootsFinset_one {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Finite L] [Algebra K L] {n : ℕ} (hn : n ≠ 0) : ↑(intermediateField K L n) = insert 0 ↑(Polynomial.nthRootsFinset (Nat.card K ^ n - 1) 1)

theorem FiniteField.adjoin_eq_intermediateField_of_isPrimitiveRoot {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Finite L] [Algebra K L] {n : ℕ} (hn : n ≠ 0) {ζ : L} (hζ : IsPrimitiveRoot ζ (Nat.card K ^ n - 1)) : K⟮ζ⟯ = intermediateField K L n

theorem FiniteField.degree_minpoly_of_isPrimitiveRoot {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Finite L] [Algebra K L] {n : ℕ} (hn : n ≠ 0) {ζ : L} (hζ : IsPrimitiveRoot ζ (Nat.card K ^ n - 1)) : (minpoly K ζ).natDegree = n

The minimal polynomial of a primitive (q^n-1)-st root of unity has degree n.

theorem FiniteField.rootsOfUnity_eq_top (F : Type u_3) [Field F] [Finite F] : rootsOfUnity (Nat.card F - 1) F = ⊤

instance FiniteField.instHasEnoughRootsOfUnityHSubNatCardOfNat_classFieldTheory (F : Type u_3) [Field F] [Finite F] : HasEnoughRootsOfUnity F (Nat.card F - 1)