[GOAL]
K : Type u_1
F : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
inst✝¹ : Field F
inst✝ : Algebra F K
⊢ Splits (algebraMap F K) (X ^ Fintype.card K - X)
[PROOFSTEP]
have h : (X ^ Fintype.card K - X : K[X]).natDegree = Fintype.card K :=
  FiniteField.X_pow_card_sub_X_natDegree_eq K Fintype.one_lt_card
[GOAL]
K : Type u_1
F : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
inst✝¹ : Field F
inst✝ : Algebra F K
h : natDegree (X ^ Fintype.card K - X) = Fintype.card K
⊢ Splits (algebraMap F K) (X ^ Fintype.card K - X)
[PROOFSTEP]
rw [← splits_id_iff_splits, splits_iff_card_roots, Polynomial.map_sub, Polynomial.map_pow, map_X, h,
  FiniteField.roots_X_pow_card_sub_X K, ← Finset.card_def, Finset.card_univ]
[GOAL]
K : Type u_1
F : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
inst✝¹ : Field F
inst✝ : Algebra F K
⊢ Algebra.adjoin F (rootSet (X ^ Fintype.card K - X) K) = ⊤
[PROOFSTEP]
classical
trans Algebra.adjoin F ((roots (X ^ Fintype.card K - X : K[X])).toFinset : Set K)
· simp only [rootSet, Polynomial.map_pow, map_X, Polynomial.map_sub]
· rw [FiniteField.roots_X_pow_card_sub_X, val_toFinset, coe_univ, Algebra.adjoin_univ]
[GOAL]
K : Type u_1
F : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
inst✝¹ : Field F
inst✝ : Algebra F K
⊢ Algebra.adjoin F (rootSet (X ^ Fintype.card K - X) K) = ⊤
[PROOFSTEP]
trans Algebra.adjoin F ((roots (X ^ Fintype.card K - X : K[X])).toFinset : Set K)
[GOAL]
K : Type u_1
F : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
inst✝¹ : Field F
inst✝ : Algebra F K
⊢ Algebra.adjoin F (rootSet (X ^ Fintype.card K - X) K) =
    Algebra.adjoin F ↑(Multiset.toFinset (roots (X ^ Fintype.card K - X)))
[PROOFSTEP]
simp only [rootSet, Polynomial.map_pow, map_X, Polynomial.map_sub]
[GOAL]
K : Type u_1
F : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
inst✝¹ : Field F
inst✝ : Algebra F K
⊢ Algebra.adjoin F ↑(Multiset.toFinset (roots (X ^ Fintype.card K - X))) = ⊤
[PROOFSTEP]
rw [FiniteField.roots_X_pow_card_sub_X, val_toFinset, coe_univ, Algebra.adjoin_univ]
[GOAL]
K : Type u_1
inst✝¹ : Field K
p q : ℕ
inst✝ : CharP K p
h : p ∣ q
⊢ Separable (X ^ q - X)
[PROOFSTEP]
use 1, X ^ q - X - 1
[GOAL]
case h
K : Type u_1
inst✝¹ : Field K
p q : ℕ
inst✝ : CharP K p
h : p ∣ q
⊢ 1 * (X ^ q - X) + (X ^ q - X - 1) * ↑derivative (X ^ q - X) = 1
[PROOFSTEP]
rw [← CharP.cast_eq_zero_iff K[X] p] at h 
[GOAL]
case h
K : Type u_1
inst✝¹ : Field K
p q : ℕ
inst✝ : CharP K p
h : ↑q = 0
⊢ 1 * (X ^ q - X) + (X ^ q - X - 1) * ↑derivative (X ^ q - X) = 1
[PROOFSTEP]
rw [derivative_sub, derivative_X_pow, derivative_X, C_eq_nat_cast, h]
[GOAL]
case h
K : Type u_1
inst✝¹ : Field K
p q : ℕ
inst✝ : CharP K p
h : ↑q = 0
⊢ 1 * (X ^ q - X) + (X ^ q - X - 1) * (0 * X ^ (q - 1) - 1) = 1
[PROOFSTEP]
ring
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝ p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
⊢ CharP (ZMod p) p
[PROOFSTEP]
infer_instance
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝ p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
⊢ FiniteDimensional (ZMod p) (GaloisField p n)
[PROOFSTEP]
dsimp only [GaloisField]
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝ p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
⊢ FiniteDimensional (ZMod p) (SplittingField (X ^ p ^ n - X))
[PROOFSTEP]
infer_instance
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝ p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
⊢ Fintype (GaloisField p n)
[PROOFSTEP]
dsimp only [GaloisField]
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝ p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
⊢ Fintype (SplittingField (X ^ p ^ n - X))
[PROOFSTEP]
exact FiniteDimensional.fintypeOfFintype (ZMod p) (GaloisField p n)
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝¹ p : ℕ
h_prime : Fact (Nat.Prime p)
n✝ n : ℕ
h : n ≠ 0
⊢ FiniteDimensional.finrank (ZMod p) (GaloisField p n) = n
[PROOFSTEP]
set g_poly := (X ^ p ^ n - X : (ZMod p)[X])
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝¹ p : ℕ
h_prime : Fact (Nat.Prime p)
n✝ n : ℕ
h : n ≠ 0
g_poly : (ZMod p)[X] := X ^ p ^ n - X
⊢ FiniteDimensional.finrank (ZMod p) (GaloisField p n) = n
[PROOFSTEP]
have hp : 1 < p := h_prime.out.one_lt
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝¹ p : ℕ
h_prime : Fact (Nat.Prime p)
n✝ n : ℕ
h : n ≠ 0
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
⊢ FiniteDimensional.finrank (ZMod p) (GaloisField p n) = n
[PROOFSTEP]
have aux : g_poly ≠ 0 := FiniteField.X_pow_card_pow_sub_X_ne_zero _ h hp
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝¹ p : ℕ
h_prime : Fact (Nat.Prime p)
n✝ n : ℕ
h : n ≠ 0
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
⊢ FiniteDimensional.finrank (ZMod p) (GaloisField p n) = n
[PROOFSTEP]
have key : Fintype.card (g_poly.rootSet (GaloisField p n)) = g_poly.natDegree :=
  card_rootSet_eq_natDegree (galois_poly_separable p _ (dvd_pow (dvd_refl p) h))
    (SplittingField.splits (X ^ p ^ n - X : (ZMod p)[X]))
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝¹ p : ℕ
h_prime : Fact (Nat.Prime p)
n✝ n : ℕ
h : n ≠ 0
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField p n)) = natDegree g_poly
⊢ FiniteDimensional.finrank (ZMod p) (GaloisField p n) = n
[PROOFSTEP]
have nat_degree_eq : g_poly.natDegree = p ^ n := FiniteField.X_pow_card_pow_sub_X_natDegree_eq _ h hp
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝¹ p : ℕ
h_prime : Fact (Nat.Prime p)
n✝ n : ℕ
h : n ≠ 0
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField p n)) = natDegree g_poly
nat_degree_eq : natDegree g_poly = p ^ n
⊢ FiniteDimensional.finrank (ZMod p) (GaloisField p n) = n
[PROOFSTEP]
rw [nat_degree_eq] at key 
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝¹ p : ℕ
h_prime : Fact (Nat.Prime p)
n✝ n : ℕ
h : n ≠ 0
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField p n)) = p ^ n
nat_degree_eq : natDegree g_poly = p ^ n
⊢ FiniteDimensional.finrank (ZMod p) (GaloisField p n) = n
[PROOFSTEP]
suffices g_poly.rootSet (GaloisField p n) = Set.univ
  by
  simp_rw [this, ← Fintype.ofEquiv_card (Equiv.Set.univ _)] at key 
  rw [@card_eq_pow_finrank (ZMod p) _ _ _ _ _ (_), ZMod.card] at key 
  exact Nat.pow_right_injective (Nat.Prime.one_lt' p).out key
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝¹ p : ℕ
h_prime : Fact (Nat.Prime p)
n✝ n : ℕ
h : n ≠ 0
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField p n)) = p ^ n
nat_degree_eq : natDegree g_poly = p ^ n
this : rootSet g_poly (GaloisField p n) = Set.univ
⊢ FiniteDimensional.finrank (ZMod p) (GaloisField p n) = n
[PROOFSTEP]
simp_rw [this, ← Fintype.ofEquiv_card (Equiv.Set.univ _)] at key 
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝¹ p : ℕ
h_prime : Fact (Nat.Prime p)
n✝ n : ℕ
h : n ≠ 0
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
nat_degree_eq : natDegree g_poly = p ^ n
this : rootSet g_poly (GaloisField p n) = Set.univ
key : Fintype.card (GaloisField p n) = p ^ n
⊢ FiniteDimensional.finrank (ZMod p) (GaloisField p n) = n
[PROOFSTEP]
rw [@card_eq_pow_finrank (ZMod p) _ _ _ _ _ (_), ZMod.card] at key 
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝¹ p : ℕ
h_prime : Fact (Nat.Prime p)
n✝ n : ℕ
h : n ≠ 0
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
nat_degree_eq : natDegree g_poly = p ^ n
this : rootSet g_poly (GaloisField p n) = Set.univ
key✝ : Fintype.card (GaloisField p n) = p ^ n
key : p ^ FiniteDimensional.finrank (ZMod p) (GaloisField p n) = p ^ n
⊢ FiniteDimensional.finrank (ZMod p) (GaloisField p n) = n
[PROOFSTEP]
exact Nat.pow_right_injective (Nat.Prime.one_lt' p).out key
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝¹ p : ℕ
h_prime : Fact (Nat.Prime p)
n✝ n : ℕ
h : n ≠ 0
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField p n)) = p ^ n
nat_degree_eq : natDegree g_poly = p ^ n
⊢ rootSet g_poly (GaloisField p n) = Set.univ
[PROOFSTEP]
rw [Set.eq_univ_iff_forall]
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝¹ p : ℕ
h_prime : Fact (Nat.Prime p)
n✝ n : ℕ
h : n ≠ 0
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField p n)) = p ^ n
nat_degree_eq : natDegree g_poly = p ^ n
⊢ ∀ (x : GaloisField p n), x ∈ rootSet g_poly (GaloisField p n)
[PROOFSTEP]
suffices
  ∀ (x) (hx : x ∈ (⊤ : Subalgebra (ZMod p) (GaloisField p n))),
    x ∈ (X ^ p ^ n - X : (ZMod p)[X]).rootSet (GaloisField p n)
  by simpa
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝¹ p : ℕ
h_prime : Fact (Nat.Prime p)
n✝ n : ℕ
h : n ≠ 0
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField p n)) = p ^ n
nat_degree_eq : natDegree g_poly = p ^ n
this : ∀ (x : GaloisField p n), x ∈ ⊤ → x ∈ rootSet (X ^ p ^ n - X) (GaloisField p n)
⊢ ∀ (x : GaloisField p n), x ∈ rootSet g_poly (GaloisField p n)
[PROOFSTEP]
simpa
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝¹ p : ℕ
h_prime : Fact (Nat.Prime p)
n✝ n : ℕ
h : n ≠ 0
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField p n)) = p ^ n
nat_degree_eq : natDegree g_poly = p ^ n
⊢ ∀ (x : GaloisField p n), x ∈ ⊤ → x ∈ rootSet (X ^ p ^ n - X) (GaloisField p n)
[PROOFSTEP]
rw [← SplittingField.adjoin_rootSet]
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝¹ p : ℕ
h_prime : Fact (Nat.Prime p)
n✝ n : ℕ
h : n ≠ 0
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField p n)) = p ^ n
nat_degree_eq : natDegree g_poly = p ^ n
⊢ ∀ (x : GaloisField p n),
    x ∈ Algebra.adjoin (ZMod p) (rootSet (X ^ p ^ n - X) (SplittingField (X ^ p ^ n - X))) →
      x ∈ rootSet (X ^ p ^ n - X) (GaloisField p n)
[PROOFSTEP]
simp_rw [Algebra.mem_adjoin_iff]
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝¹ p : ℕ
h_prime : Fact (Nat.Prime p)
n✝ n : ℕ
h : n ≠ 0
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField p n)) = p ^ n
nat_degree_eq : natDegree g_poly = p ^ n
⊢ ∀ (x : GaloisField p n),
    x ∈
        Subring.closure
          (Set.range ↑(algebraMap (ZMod p) (GaloisField p n)) ∪
            rootSet (X ^ p ^ n - X) (SplittingField (X ^ p ^ n - X))) →
      x ∈ rootSet (X ^ p ^ n - X) (GaloisField p n)
[PROOFSTEP]
intro x hx
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝¹ p : ℕ
h_prime : Fact (Nat.Prime p)
n✝ n : ℕ
h : n ≠ 0
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField p n)) = p ^ n
nat_degree_eq : natDegree g_poly = p ^ n
x : GaloisField p n
hx :
  x ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod p) (GaloisField p n)) ∪ rootSet (X ^ p ^ n - X) (SplittingField (X ^ p ^ n - X)))
⊢ x ∈ rootSet (X ^ p ^ n - X) (GaloisField p n)
[PROOFSTEP]
cases p
[GOAL]
case zero
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝¹ n✝ n : ℕ
h : n ≠ 0
h_prime : Fact (Nat.Prime Nat.zero)
g_poly : (ZMod Nat.zero)[X] := X ^ Nat.zero ^ n - X
hp : 1 < Nat.zero
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField Nat.zero n)) = Nat.zero ^ n
nat_degree_eq : natDegree g_poly = Nat.zero ^ n
x : GaloisField Nat.zero n
hx :
  x ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod Nat.zero) (GaloisField Nat.zero n)) ∪
        rootSet (X ^ Nat.zero ^ n - X) (SplittingField (X ^ Nat.zero ^ n - X)))
⊢ x ∈ rootSet (X ^ Nat.zero ^ n - X) (GaloisField Nat.zero n)
case succ
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree g_poly = Nat.succ n✝ ^ n
x : GaloisField (Nat.succ n✝) n
hx :
  x ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
⊢ x ∈ rootSet (X ^ Nat.succ n✝ ^ n - X) (GaloisField (Nat.succ n✝) n)
[PROOFSTEP]
cases hp
[GOAL]
case succ
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree g_poly = Nat.succ n✝ ^ n
x : GaloisField (Nat.succ n✝) n
hx :
  x ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
⊢ x ∈ rootSet (X ^ Nat.succ n✝ ^ n - X) (GaloisField (Nat.succ n✝) n)
[PROOFSTEP]
refine Subring.closure_induction hx ?_ ?_ ?_ ?_ ?_ ?_
[GOAL]
case succ.refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree g_poly = Nat.succ n✝ ^ n
x : GaloisField (Nat.succ n✝) n
hx :
  x ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
⊢ ∀ (x : GaloisField (Nat.succ n✝) n),
    x ∈
        Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
          rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)) →
      x ∈ rootSet (X ^ Nat.succ n✝ ^ n - X) (GaloisField (Nat.succ n✝) n)
[PROOFSTEP]
simp_rw [mem_rootSet_of_ne aux]
[GOAL]
case succ.refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree g_poly = Nat.succ n✝ ^ n
x : GaloisField (Nat.succ n✝) n
hx :
  x ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
⊢ 0 ∈ rootSet (X ^ Nat.succ n✝ ^ n - X) (GaloisField (Nat.succ n✝) n)
[PROOFSTEP]
simp_rw [mem_rootSet_of_ne aux]
[GOAL]
case succ.refine_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree g_poly = Nat.succ n✝ ^ n
x : GaloisField (Nat.succ n✝) n
hx :
  x ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
⊢ 1 ∈ rootSet (X ^ Nat.succ n✝ ^ n - X) (GaloisField (Nat.succ n✝) n)
[PROOFSTEP]
simp_rw [mem_rootSet_of_ne aux]
[GOAL]
case succ.refine_4
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree g_poly = Nat.succ n✝ ^ n
x : GaloisField (Nat.succ n✝) n
hx :
  x ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
⊢ ∀ (x y : GaloisField (Nat.succ n✝) n),
    x ∈ rootSet (X ^ Nat.succ n✝ ^ n - X) (GaloisField (Nat.succ n✝) n) →
      y ∈ rootSet (X ^ Nat.succ n✝ ^ n - X) (GaloisField (Nat.succ n✝) n) →
        x + y ∈ rootSet (X ^ Nat.succ n✝ ^ n - X) (GaloisField (Nat.succ n✝) n)
[PROOFSTEP]
simp_rw [mem_rootSet_of_ne aux]
[GOAL]
case succ.refine_5
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree g_poly = Nat.succ n✝ ^ n
x : GaloisField (Nat.succ n✝) n
hx :
  x ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
⊢ ∀ (x : GaloisField (Nat.succ n✝) n),
    x ∈ rootSet (X ^ Nat.succ n✝ ^ n - X) (GaloisField (Nat.succ n✝) n) →
      -x ∈ rootSet (X ^ Nat.succ n✝ ^ n - X) (GaloisField (Nat.succ n✝) n)
[PROOFSTEP]
simp_rw [mem_rootSet_of_ne aux]
[GOAL]
case succ.refine_6
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree g_poly = Nat.succ n✝ ^ n
x : GaloisField (Nat.succ n✝) n
hx :
  x ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
⊢ ∀ (x y : GaloisField (Nat.succ n✝) n),
    x ∈ rootSet (X ^ Nat.succ n✝ ^ n - X) (GaloisField (Nat.succ n✝) n) →
      y ∈ rootSet (X ^ Nat.succ n✝ ^ n - X) (GaloisField (Nat.succ n✝) n) →
        x * y ∈ rootSet (X ^ Nat.succ n✝ ^ n - X) (GaloisField (Nat.succ n✝) n)
[PROOFSTEP]
simp_rw [mem_rootSet_of_ne aux]
[GOAL]
case succ.refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree g_poly = Nat.succ n✝ ^ n
x : GaloisField (Nat.succ n✝) n
hx :
  x ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
⊢ ∀ (x : GaloisField (Nat.succ n✝) n),
    x ∈
        Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
          rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)) →
      ↑(aeval x) (X ^ Nat.succ n✝ ^ n - X) = 0
[PROOFSTEP]
rintro x (⟨r, rfl⟩ | hx)
[GOAL]
case succ.refine_1.inl.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree g_poly = Nat.succ n✝ ^ n
x : GaloisField (Nat.succ n✝) n
hx :
  x ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
r : ZMod (Nat.succ n✝)
⊢ ↑(aeval (↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) r)) (X ^ Nat.succ n✝ ^ n - X) = 0
[PROOFSTEP]
simp only [map_sub, map_pow, aeval_X]
[GOAL]
case succ.refine_1.inl.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree g_poly = Nat.succ n✝ ^ n
x : GaloisField (Nat.succ n✝) n
hx :
  x ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
r : ZMod (Nat.succ n✝)
⊢ ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) r ^ Nat.succ n✝ ^ n -
      ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) r =
    0
[PROOFSTEP]
rw [← map_pow, ZMod.pow_card_pow, sub_self]
[GOAL]
case succ.refine_1.inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree g_poly = Nat.succ n✝ ^ n
x✝ : GaloisField (Nat.succ n✝) n
hx✝ :
  x✝ ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
x : GaloisField (Nat.succ n✝) n
hx : x ∈ rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X))
⊢ ↑(aeval x) (X ^ Nat.succ n✝ ^ n - X) = 0
[PROOFSTEP]
dsimp only [GaloisField] at hx 
[GOAL]
case succ.refine_1.inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree g_poly = Nat.succ n✝ ^ n
x✝ : GaloisField (Nat.succ n✝) n
hx✝ :
  x✝ ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
x : GaloisField (Nat.succ n✝) n
hx : x ∈ rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X))
⊢ ↑(aeval x) (X ^ Nat.succ n✝ ^ n - X) = 0
[PROOFSTEP]
rwa [mem_rootSet_of_ne aux] at hx 
[GOAL]
case succ.refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree g_poly = Nat.succ n✝ ^ n
x : GaloisField (Nat.succ n✝) n
hx :
  x ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
⊢ ↑(aeval 0) (X ^ Nat.succ n✝ ^ n - X) = 0
[PROOFSTEP]
rw [← coeff_zero_eq_aeval_zero']
[GOAL]
case succ.refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree g_poly = Nat.succ n✝ ^ n
x : GaloisField (Nat.succ n✝) n
hx :
  x ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
⊢ ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) (coeff (X ^ Nat.succ n✝ ^ n - X) 0) = 0
[PROOFSTEP]
simp only [coeff_X_pow, coeff_X_zero, sub_zero, _root_.map_eq_zero, ite_eq_right_iff, one_ne_zero, coeff_sub]
[GOAL]
case succ.refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree g_poly = Nat.succ n✝ ^ n
x : GaloisField (Nat.succ n✝) n
hx :
  x ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
⊢ 0 = Nat.succ n✝ ^ n → False
[PROOFSTEP]
intro hn
[GOAL]
case succ.refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree g_poly = Nat.succ n✝ ^ n
x : GaloisField (Nat.succ n✝) n
hx :
  x ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
hn : 0 = Nat.succ n✝ ^ n
⊢ False
[PROOFSTEP]
exact Nat.not_lt_zero 1 (pow_eq_zero hn.symm ▸ hp)
[GOAL]
case succ.refine_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree g_poly = Nat.succ n✝ ^ n
x : GaloisField (Nat.succ n✝) n
hx :
  x ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
⊢ ↑(aeval 1) (X ^ Nat.succ n✝ ^ n - X) = 0
[PROOFSTEP]
simp
[GOAL]
case succ.refine_4
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree g_poly = Nat.succ n✝ ^ n
x : GaloisField (Nat.succ n✝) n
hx :
  x ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
⊢ ∀ (x y : GaloisField (Nat.succ n✝) n),
    ↑(aeval x) (X ^ Nat.succ n✝ ^ n - X) = 0 →
      ↑(aeval y) (X ^ Nat.succ n✝ ^ n - X) = 0 → ↑(aeval (x + y)) (X ^ Nat.succ n✝ ^ n - X) = 0
[PROOFSTEP]
simp only [aeval_X_pow, aeval_X, AlgHom.map_sub, add_pow_char_pow, sub_eq_zero]
[GOAL]
case succ.refine_4
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree g_poly = Nat.succ n✝ ^ n
x : GaloisField (Nat.succ n✝) n
hx :
  x ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
⊢ ∀ (x y : GaloisField (Nat.succ n✝) n),
    x ^ Nat.succ n✝ ^ n = x → y ^ Nat.succ n✝ ^ n = y → x ^ Nat.succ n✝ ^ n + y ^ Nat.succ n✝ ^ n = x + y
[PROOFSTEP]
intro x y hx hy
[GOAL]
case succ.refine_4
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree g_poly = Nat.succ n✝ ^ n
x✝ : GaloisField (Nat.succ n✝) n
hx✝ :
  x✝ ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
x y : GaloisField (Nat.succ n✝) n
hx : x ^ Nat.succ n✝ ^ n = x
hy : y ^ Nat.succ n✝ ^ n = y
⊢ x ^ Nat.succ n✝ ^ n + y ^ Nat.succ n✝ ^ n = x + y
[PROOFSTEP]
rw [hx, hy]
[GOAL]
case succ.refine_5
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree g_poly = Nat.succ n✝ ^ n
x : GaloisField (Nat.succ n✝) n
hx :
  x ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
⊢ ∀ (x : GaloisField (Nat.succ n✝) n),
    ↑(aeval x) (X ^ Nat.succ n✝ ^ n - X) = 0 → ↑(aeval (-x)) (X ^ Nat.succ n✝ ^ n - X) = 0
[PROOFSTEP]
intro x hx
[GOAL]
case succ.refine_5
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree g_poly = Nat.succ n✝ ^ n
x✝ : GaloisField (Nat.succ n✝) n
hx✝ :
  x✝ ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
x : GaloisField (Nat.succ n✝) n
hx : ↑(aeval x) (X ^ Nat.succ n✝ ^ n - X) = 0
⊢ ↑(aeval (-x)) (X ^ Nat.succ n✝ ^ n - X) = 0
[PROOFSTEP]
simp only [sub_eq_zero, aeval_X_pow, aeval_X, AlgHom.map_sub, sub_neg_eq_add] at *
[GOAL]
case succ.refine_5
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : X ^ Nat.succ n✝ ^ n - X ≠ 0
key : Fintype.card ↑(rootSet (X ^ Nat.succ n✝ ^ n - X) (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree (X ^ Nat.succ n✝ ^ n - X) = Nat.succ n✝ ^ n
x✝ : GaloisField (Nat.succ n✝) n
hx✝ :
  x✝ ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
x : GaloisField (Nat.succ n✝) n
hx : x ^ Nat.succ n✝ ^ n = x
⊢ (-x) ^ Nat.succ n✝ ^ n + x = 0
[PROOFSTEP]
rw [neg_pow, hx, CharP.neg_one_pow_char_pow]
[GOAL]
case succ.refine_5
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : X ^ Nat.succ n✝ ^ n - X ≠ 0
key : Fintype.card ↑(rootSet (X ^ Nat.succ n✝ ^ n - X) (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree (X ^ Nat.succ n✝ ^ n - X) = Nat.succ n✝ ^ n
x✝ : GaloisField (Nat.succ n✝) n
hx✝ :
  x✝ ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
x : GaloisField (Nat.succ n✝) n
hx : x ^ Nat.succ n✝ ^ n = x
⊢ -1 * x + x = 0
[PROOFSTEP]
simp
[GOAL]
case succ.refine_6
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree g_poly = Nat.succ n✝ ^ n
x : GaloisField (Nat.succ n✝) n
hx :
  x ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
⊢ ∀ (x y : GaloisField (Nat.succ n✝) n),
    ↑(aeval x) (X ^ Nat.succ n✝ ^ n - X) = 0 →
      ↑(aeval y) (X ^ Nat.succ n✝ ^ n - X) = 0 → ↑(aeval (x * y)) (X ^ Nat.succ n✝ ^ n - X) = 0
[PROOFSTEP]
simp only [aeval_X_pow, aeval_X, AlgHom.map_sub, mul_pow, sub_eq_zero]
[GOAL]
case succ.refine_6
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree g_poly = Nat.succ n✝ ^ n
x : GaloisField (Nat.succ n✝) n
hx :
  x ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
⊢ ∀ (x y : GaloisField (Nat.succ n✝) n),
    x ^ Nat.succ n✝ ^ n = x → y ^ Nat.succ n✝ ^ n = y → x ^ Nat.succ n✝ ^ n * y ^ Nat.succ n✝ ^ n = x * y
[PROOFSTEP]
intro x y hx hy
[GOAL]
case succ.refine_6
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝² n✝¹ n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
g_poly : (ZMod (Nat.succ n✝))[X] := X ^ Nat.succ n✝ ^ n - X
hp : 1 < Nat.succ n✝
aux : g_poly ≠ 0
key : Fintype.card ↑(rootSet g_poly (GaloisField (Nat.succ n✝) n)) = Nat.succ n✝ ^ n
nat_degree_eq : natDegree g_poly = Nat.succ n✝ ^ n
x✝ : GaloisField (Nat.succ n✝) n
hx✝ :
  x✝ ∈
    Subring.closure
      (Set.range ↑(algebraMap (ZMod (Nat.succ n✝)) (GaloisField (Nat.succ n✝) n)) ∪
        rootSet (X ^ Nat.succ n✝ ^ n - X) (SplittingField (X ^ Nat.succ n✝ ^ n - X)))
x y : GaloisField (Nat.succ n✝) n
hx : x ^ Nat.succ n✝ ^ n = x
hy : y ^ Nat.succ n✝ ^ n = y
⊢ x ^ Nat.succ n✝ ^ n * y ^ Nat.succ n✝ ^ n = x * y
[PROOFSTEP]
rw [hx, hy]
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝ p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
⊢ Fintype.card (GaloisField p n) = p ^ n
[PROOFSTEP]
let b := IsNoetherian.finsetBasis (ZMod p) (GaloisField p n)
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝ p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) (GaloisField p n) } (ZMod p) (GaloisField p n) :=
  IsNoetherian.finsetBasis (ZMod p) (GaloisField p n)
⊢ Fintype.card (GaloisField p n) = p ^ n
[PROOFSTEP]
rw [Module.card_fintype b, ← FiniteDimensional.finrank_eq_card_basis b, ZMod.card, finrank p h]
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝ p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
⊢ Splits (RingHom.id (ZMod p)) (X ^ p - X)
[PROOFSTEP]
have hp : 1 < p := h_prime.out.one_lt
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝ p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
hp : 1 < p
⊢ Splits (RingHom.id (ZMod p)) (X ^ p - X)
[PROOFSTEP]
have h1 : roots (X ^ p - X : (ZMod p)[X]) = Finset.univ.val :=
  by
  convert FiniteField.roots_X_pow_card_sub_X (ZMod p)
  exact (ZMod.card p).symm
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝ p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
hp : 1 < p
⊢ roots (X ^ p - X) = univ.val
[PROOFSTEP]
convert FiniteField.roots_X_pow_card_sub_X (ZMod p)
[GOAL]
case h.e'_2.h.e'_4.h.h.e'_5.h.e'_6
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝ p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
hp : 1 < p
e_2✝ : ZMod.commRing p = EuclideanDomain.toCommRing
⊢ p = Fintype.card (ZMod p)
[PROOFSTEP]
exact (ZMod.card p).symm
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝ p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
hp : 1 < p
h1 : roots (X ^ p - X) = univ.val
⊢ Splits (RingHom.id (ZMod p)) (X ^ p - X)
[PROOFSTEP]
have h2 := FiniteField.X_pow_card_sub_X_natDegree_eq (ZMod p) hp
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝ p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
hp : 1 < p
h1 : roots (X ^ p - X) = univ.val
h2 : natDegree (X ^ p - X) = p
⊢ Splits (RingHom.id (ZMod p)) (X ^ p - X)
[PROOFSTEP]
cases p
[GOAL]
case zero
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝ n : ℕ
h_prime : Fact (Nat.Prime Nat.zero)
hp : 1 < Nat.zero
h1 : roots (X ^ Nat.zero - X) = univ.val
h2 : natDegree (X ^ Nat.zero - X) = Nat.zero
⊢ Splits (RingHom.id (ZMod Nat.zero)) (X ^ Nat.zero - X)
case succ
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝¹ n n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
hp : 1 < Nat.succ n✝
h1 : roots (X ^ Nat.succ n✝ - X) = univ.val
h2 : natDegree (X ^ Nat.succ n✝ - X) = Nat.succ n✝
⊢ Splits (RingHom.id (ZMod (Nat.succ n✝))) (X ^ Nat.succ n✝ - X)
[PROOFSTEP]
cases hp
[GOAL]
case succ
p : ℕ
inst✝ : Fact (Nat.Prime p)
n✝¹ n n✝ : ℕ
h_prime : Fact (Nat.Prime (Nat.succ n✝))
hp : 1 < Nat.succ n✝
h1 : roots (X ^ Nat.succ n✝ - X) = univ.val
h2 : natDegree (X ^ Nat.succ n✝ - X) = Nat.succ n✝
⊢ Splits (RingHom.id (ZMod (Nat.succ n✝))) (X ^ Nat.succ n✝ - X)
[PROOFSTEP]
rw [splits_iff_card_roots, h1, ← Finset.card_def, Finset.card_univ, h2, ZMod.card]
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝ p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
⊢ X ^ p ^ 1 = X ^ Fintype.card (ZMod p)
[PROOFSTEP]
rw [pow_one, ZMod.card p]
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝ p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : X ^ p ^ 1 = X ^ Fintype.card (ZMod p) :=
  Eq.mpr (id (pow_one p ▸ Eq.refl (X ^ p ^ 1 = X ^ Fintype.card (ZMod p))))
    (Eq.mpr (id (ZMod.card p ▸ Eq.refl (X ^ p = X ^ Fintype.card (ZMod p)))) (Eq.refl (X ^ p)))
⊢ IsSplittingField (ZMod p) (ZMod p) (X ^ p ^ 1 - X)
[PROOFSTEP]
rw [h]
[GOAL]
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝ p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : X ^ p ^ 1 = X ^ Fintype.card (ZMod p) :=
  Eq.mpr (id (pow_one p ▸ Eq.refl (X ^ p ^ 1 = X ^ Fintype.card (ZMod p))))
    (Eq.mpr (id (ZMod.card p ▸ Eq.refl (X ^ p = X ^ Fintype.card (ZMod p)))) (Eq.refl (X ^ p)))
⊢ IsSplittingField (ZMod p) (ZMod p) (X ^ Fintype.card (ZMod p) - X)
[PROOFSTEP]
infer_instance
[GOAL]
p✝ : ℕ
inst✝⁷ : Fact (Nat.Prime p✝)
n✝ p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K✝ : Type u_1
inst✝⁶ : Field K✝
inst✝⁵ : Fintype K✝
inst✝⁴ : Algebra (ZMod p) K✝
K : Type u_2
K' : Type u_3
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Finite K'
inst✝ : Algebra K K'
⊢ IsGalois K K'
[PROOFSTEP]
cases nonempty_fintype K'
[GOAL]
case intro
p✝ : ℕ
inst✝⁷ : Fact (Nat.Prime p✝)
n✝ p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K✝ : Type u_1
inst✝⁶ : Field K✝
inst✝⁵ : Fintype K✝
inst✝⁴ : Algebra (ZMod p) K✝
K : Type u_2
K' : Type u_3
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Finite K'
inst✝ : Algebra K K'
val✝ : Fintype K'
⊢ IsGalois K K'
[PROOFSTEP]
obtain ⟨p, hp⟩ := CharP.exists K
[GOAL]
case intro.intro
p✝¹ : ℕ
inst✝⁷ : Fact (Nat.Prime p✝¹)
n✝ p✝ : ℕ
h_prime : Fact (Nat.Prime p✝)
n : ℕ
K✝ : Type u_1
inst✝⁶ : Field K✝
inst✝⁵ : Fintype K✝
inst✝⁴ : Algebra (ZMod p✝) K✝
K : Type u_2
K' : Type u_3
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Finite K'
inst✝ : Algebra K K'
val✝ : Fintype K'
p : ℕ
hp : CharP K p
⊢ IsGalois K K'
[PROOFSTEP]
haveI : CharP K p := hp
[GOAL]
case intro.intro
p✝¹ : ℕ
inst✝⁷ : Fact (Nat.Prime p✝¹)
n✝ p✝ : ℕ
h_prime : Fact (Nat.Prime p✝)
n : ℕ
K✝ : Type u_1
inst✝⁶ : Field K✝
inst✝⁵ : Fintype K✝
inst✝⁴ : Algebra (ZMod p✝) K✝
K : Type u_2
K' : Type u_3
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Finite K'
inst✝ : Algebra K K'
val✝ : Fintype K'
p : ℕ
hp : CharP K p
this : CharP K p
⊢ IsGalois K K'
[PROOFSTEP]
haveI : CharP K' p := charP_of_injective_algebraMap' K K' p
[GOAL]
case intro.intro
p✝¹ : ℕ
inst✝⁷ : Fact (Nat.Prime p✝¹)
n✝ p✝ : ℕ
h_prime : Fact (Nat.Prime p✝)
n : ℕ
K✝ : Type u_1
inst✝⁶ : Field K✝
inst✝⁵ : Fintype K✝
inst✝⁴ : Algebra (ZMod p✝) K✝
K : Type u_2
K' : Type u_3
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Finite K'
inst✝ : Algebra K K'
val✝ : Fintype K'
p : ℕ
hp : CharP K p
this✝ : CharP K p
this : CharP K' p
⊢ IsGalois K K'
[PROOFSTEP]
exact
  IsGalois.of_separable_splitting_field
    (galois_poly_separable p (Fintype.card K')
      (let ⟨n, _, hn⟩ := FiniteField.card K' p
      hn.symm ▸ dvd_pow_self p n.ne_zero))
[GOAL]
p✝ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝)
n : ℕ
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : Fintype K
K' : Type u_2
inst✝³ : Field K'
inst✝² : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
⊢ K ≃ₐ[ZMod p] K'
[PROOFSTEP]
have : CharP K p := by rw [← Algebra.charP_iff (ZMod p) K p]; exact ZMod.charP p
[GOAL]
p✝ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝)
n : ℕ
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : Fintype K
K' : Type u_2
inst✝³ : Field K'
inst✝² : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
⊢ CharP K p
[PROOFSTEP]
rw [← Algebra.charP_iff (ZMod p) K p]
[GOAL]
p✝ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝)
n : ℕ
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : Fintype K
K' : Type u_2
inst✝³ : Field K'
inst✝² : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
⊢ CharP (ZMod p) p
[PROOFSTEP]
exact ZMod.charP p
[GOAL]
p✝ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝)
n : ℕ
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : Fintype K
K' : Type u_2
inst✝³ : Field K'
inst✝² : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
this : CharP K p
⊢ K ≃ₐ[ZMod p] K'
[PROOFSTEP]
have : CharP K' p := by rw [← Algebra.charP_iff (ZMod p) K' p]; exact ZMod.charP p
[GOAL]
p✝ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝)
n : ℕ
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : Fintype K
K' : Type u_2
inst✝³ : Field K'
inst✝² : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
this : CharP K p
⊢ CharP K' p
[PROOFSTEP]
rw [← Algebra.charP_iff (ZMod p) K' p]
[GOAL]
p✝ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝)
n : ℕ
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : Fintype K
K' : Type u_2
inst✝³ : Field K'
inst✝² : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
this : CharP K p
⊢ CharP (ZMod p) p
[PROOFSTEP]
exact ZMod.charP p
[GOAL]
p✝ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝)
n : ℕ
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : Fintype K
K' : Type u_2
inst✝³ : Field K'
inst✝² : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
this✝ : CharP K p
this : CharP K' p
⊢ K ≃ₐ[ZMod p] K'
[PROOFSTEP]
choose n a hK using FiniteField.card K p
[GOAL]
p✝ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : Fintype K
K' : Type u_2
inst✝³ : Field K'
inst✝² : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
this✝ : CharP K p
this : CharP K' p
n : ℕ+
a : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
⊢ K ≃ₐ[ZMod p] K'
[PROOFSTEP]
choose n' a' hK' using FiniteField.card K' p
[GOAL]
p✝ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : Fintype K
K' : Type u_2
inst✝³ : Field K'
inst✝² : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
this✝ : CharP K p
this : CharP K' p
n : ℕ+
a : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
a' : Nat.Prime p
hK' : Fintype.card K' = p ^ ↑n'
⊢ K ≃ₐ[ZMod p] K'
[PROOFSTEP]
rw [hK, hK'] at hKK' 
[GOAL]
p✝ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : Fintype K
K' : Type u_2
inst✝³ : Field K'
inst✝² : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
this✝ : CharP K p
this : CharP K' p
n : ℕ+
a : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hKK' : p ^ ↑n = p ^ ↑n'
a' : Nat.Prime p
hK' : Fintype.card K' = p ^ ↑n'
⊢ K ≃ₐ[ZMod p] K'
[PROOFSTEP]
have hGalK := GaloisField.algEquivGaloisField p n hK
[GOAL]
p✝ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : Fintype K
K' : Type u_2
inst✝³ : Field K'
inst✝² : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
this✝ : CharP K p
this : CharP K' p
n : ℕ+
a : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hKK' : p ^ ↑n = p ^ ↑n'
a' : Nat.Prime p
hK' : Fintype.card K' = p ^ ↑n'
hGalK : K ≃ₐ[ZMod p] GaloisField p ↑n
⊢ K ≃ₐ[ZMod p] K'
[PROOFSTEP]
have hK'Gal := (GaloisField.algEquivGaloisField p n' hK').symm
[GOAL]
p✝ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : Fintype K
K' : Type u_2
inst✝³ : Field K'
inst✝² : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
this✝ : CharP K p
this : CharP K' p
n : ℕ+
a : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hKK' : p ^ ↑n = p ^ ↑n'
a' : Nat.Prime p
hK' : Fintype.card K' = p ^ ↑n'
hGalK : K ≃ₐ[ZMod p] GaloisField p ↑n
hK'Gal : GaloisField p ↑n' ≃ₐ[ZMod p] K'
⊢ K ≃ₐ[ZMod p] K'
[PROOFSTEP]
rw [Nat.pow_right_injective h_prime.out.one_lt hKK'] at *
[GOAL]
p✝ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : Fintype K
K' : Type u_2
inst✝³ : Field K'
inst✝² : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
this✝ : CharP K p
this : CharP K' p
n : ℕ+
a : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hKK' : p ^ ↑n' = p ^ ↑n'
a' : Nat.Prime p
hK' : Fintype.card K' = p ^ ↑n'
hGalK : K ≃ₐ[ZMod p] GaloisField p ↑n'
hK'Gal : GaloisField p ↑n' ≃ₐ[ZMod p] K'
⊢ K ≃ₐ[ZMod p] K'
[PROOFSTEP]
exact AlgEquiv.trans hGalK hK'Gal
[GOAL]
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
n : ℕ
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
K' : Type u_2
inst✝¹ : Field K'
inst✝ : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
⊢ K ≃+* K'
[PROOFSTEP]
choose p _char_p_K using CharP.exists K
[GOAL]
p✝ : ℕ
inst✝⁴ : Fact (Nat.Prime p✝)
n : ℕ
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
K' : Type u_2
inst✝¹ : Field K'
inst✝ : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
⊢ K ≃+* K'
[PROOFSTEP]
choose p' _char_p'_K' using CharP.exists K'
[GOAL]
p✝ : ℕ
inst✝⁴ : Fact (Nat.Prime p✝)
n : ℕ
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
K' : Type u_2
inst✝¹ : Field K'
inst✝ : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p'
⊢ K ≃+* K'
[PROOFSTEP]
choose n hp hK using FiniteField.card K p
[GOAL]
p✝ : ℕ
inst✝⁴ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
K' : Type u_2
inst✝¹ : Field K'
inst✝ : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p'
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
⊢ K ≃+* K'
[PROOFSTEP]
choose n' hp' hK' using FiniteField.card K' p'
[GOAL]
p✝ : ℕ
inst✝⁴ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
K' : Type u_2
inst✝¹ : Field K'
inst✝ : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p'
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ ↑n'
⊢ K ≃+* K'
[PROOFSTEP]
have hpp' : p = p' := by
  by_contra hne
  have h2 := Nat.coprime_pow_primes n n' hp hp' hne
  rw [(Eq.congr hK hK').mp hKK', Nat.coprime_self, pow_eq_one_iff (PNat.ne_zero n')] at h2 
  exact Nat.Prime.ne_one hp' h2
[GOAL]
p✝ : ℕ
inst✝⁴ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
K' : Type u_2
inst✝¹ : Field K'
inst✝ : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p'
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ ↑n'
⊢ p = p'
[PROOFSTEP]
by_contra hne
[GOAL]
p✝ : ℕ
inst✝⁴ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
K' : Type u_2
inst✝¹ : Field K'
inst✝ : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p'
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ ↑n'
hne : ¬p = p'
⊢ False
[PROOFSTEP]
have h2 := Nat.coprime_pow_primes n n' hp hp' hne
[GOAL]
p✝ : ℕ
inst✝⁴ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
K' : Type u_2
inst✝¹ : Field K'
inst✝ : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p'
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ ↑n'
hne : ¬p = p'
h2 : Nat.coprime (p ^ ↑n) (p' ^ ↑n')
⊢ False
[PROOFSTEP]
rw [(Eq.congr hK hK').mp hKK', Nat.coprime_self, pow_eq_one_iff (PNat.ne_zero n')] at h2 
[GOAL]
p✝ : ℕ
inst✝⁴ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
K' : Type u_2
inst✝¹ : Field K'
inst✝ : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p'
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ ↑n'
hne : ¬p = p'
h2 : p' = 1
⊢ False
[PROOFSTEP]
exact Nat.Prime.ne_one hp' h2
[GOAL]
p✝ : ℕ
inst✝⁴ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
K' : Type u_2
inst✝¹ : Field K'
inst✝ : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p'
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ ↑n'
hpp' : p = p'
⊢ K ≃+* K'
[PROOFSTEP]
rw [← hpp'] at _char_p'_K' 
[GOAL]
p✝ : ℕ
inst✝⁴ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
K' : Type u_2
inst✝¹ : Field K'
inst✝ : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ ↑n'
hpp' : p = p'
⊢ K ≃+* K'
[PROOFSTEP]
haveI := fact_iff.2 hp
[GOAL]
p✝ : ℕ
inst✝⁴ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
K' : Type u_2
inst✝¹ : Field K'
inst✝ : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ ↑n'
hpp' : p = p'
this : Fact (Nat.Prime p)
⊢ K ≃+* K'
[PROOFSTEP]
letI : Algebra (ZMod p) K := ZMod.algebra _ _
[GOAL]
p✝ : ℕ
inst✝⁴ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
K' : Type u_2
inst✝¹ : Field K'
inst✝ : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ ↑n'
hpp' : p = p'
this✝ : Fact (Nat.Prime p)
this : Algebra (ZMod p) K := ZMod.algebra K p
⊢ K ≃+* K'
[PROOFSTEP]
letI : Algebra (ZMod p) K' := ZMod.algebra _ _
[GOAL]
p✝ : ℕ
inst✝⁴ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
K' : Type u_2
inst✝¹ : Field K'
inst✝ : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ ↑n'
hpp' : p = p'
this✝¹ : Fact (Nat.Prime p)
this✝ : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) K' := ZMod.algebra K' p
⊢ K ≃+* K'
[PROOFSTEP]
exact ↑(algEquivOfCardEq p hKK')
