-rw-r--r-- 1009 leangoppa-20230726/Goppadecoding/finite_perfect.lean raw
-- written by Riccardo Brasca, used with permission

import Mathlib.FieldTheory.PerfectClosure
import Mathlib.FieldTheory.Finite.Basic

variable (K : Type _) [Field K] [Fintype K] (p : ℕ) [inst : CharP K p]

theorem finite_field_is_perfect :
    have : Fact (Nat.Prime p) := ⟨CharP.char_is_prime K p⟩
    Function.Surjective (frobenius K p) := by
  intro x
  obtain ⟨n, _, hn⟩ := FiniteField.card K p
  refine' ⟨x ^ (p ^ (n - 1)), _⟩
  dsimp [frobenius]
  calc
    _ = x ^ (p ^ (↑n - 1) * p ^ 1) := by rw [← pow_mul, pow_one]
    _ = x ^ (p ^ (↑n - 1 + 1)) := by rw [pow_add]
    _ = x ^ (p ^ ((n : ℕ).pred.succ)) := by rw [Nat.pred_eq_sub_one]
    _ = x ^ (p ^ n) := by rw [Nat.succ_pred n.ne_zero]
    _ = x := by rw [← hn, FiniteField.pow_card _]

noncomputable instance  :
    have : Fact (Nat.Prime p) := ⟨CharP.char_is_prime K p⟩
    PerfectRing K p :=
  have : Fact (Nat.Prime p) := ⟨CharP.char_is_prime K p⟩
  PerfectRing.ofSurjective K _ (finite_field_is_perfect K p)