[GOAL]
K : Type u_1
R : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
inst✝ : Fintype R
p : R[X]
hp : 0 < degree p
a : R
x✝ : a ∈ image (fun x => eval x p) univ
⊢ filter (fun x => eval x p = a) univ = Multiset.toFinset (roots (p - ↑C a))
[PROOFSTEP]
simp [Finset.ext_iff, ← mem_roots_sub_C hp]
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 2
hR : Fintype.card R % 2 = 1
this : DecidableEq R := Classical.decEq R
hd : Disjoint (image (fun x => eval x f) univ) (image (fun x => eval x (-g)) univ)
⊢ 0 < degree f
[PROOFSTEP]
rw [hf2]
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 2
hR : Fintype.card R % 2 = 1
this : DecidableEq R := Classical.decEq R
hd : Disjoint (image (fun x => eval x f) univ) (image (fun x => eval x (-g)) univ)
⊢ 0 < 2
[PROOFSTEP]
exact by decide
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 2
hR : Fintype.card R % 2 = 1
this : DecidableEq R := Classical.decEq R
hd : Disjoint (image (fun x => eval x f) univ) (image (fun x => eval x (-g)) univ)
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 2
hR : Fintype.card R % 2 = 1
this : DecidableEq R := Classical.decEq R
hd : Disjoint (image (fun x => eval x f) univ) (image (fun x => eval x (-g)) univ)
⊢ ¬Fintype.card R % 2 = natDegree f * card (image (fun x => eval x f) univ) % 2
[PROOFSTEP]
simp [natDegree_eq_of_degree_eq_some hf2, hR]
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 2
hR : Fintype.card R % 2 = 1
this : DecidableEq R := Classical.decEq R
hd : Disjoint (image (fun x => eval x f) univ) (image (fun x => eval x (-g)) univ)
⊢ 0 < degree (-g)
[PROOFSTEP]
rw [degree_neg, hg2]
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 2
hR : Fintype.card R % 2 = 1
this : DecidableEq R := Classical.decEq R
hd : Disjoint (image (fun x => eval x f) univ) (image (fun x => eval x (-g)) univ)
⊢ 0 < 2
[PROOFSTEP]
exact by decide
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 2
hR : Fintype.card R % 2 = 1
this : DecidableEq R := Classical.decEq R
hd : Disjoint (image (fun x => eval x f) univ) (image (fun x => eval x (-g)) univ)
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 2
hR : Fintype.card R % 2 = 1
this : DecidableEq R := Classical.decEq R
hd : Disjoint (image (fun x => eval x f) univ) (image (fun x => eval x (-g)) univ)
⊢ natDegree f * card (image (fun x => eval x f) univ) + natDegree (-g) * card (image (fun x => eval x (-g)) univ) =
    2 * card (image (fun x => eval x f) univ ∪ image (fun x => eval x (-g)) univ)
[PROOFSTEP]
rw [card_disjoint_union hd]
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 2
hR : Fintype.card R % 2 = 1
this : DecidableEq R := Classical.decEq R
hd : Disjoint (image (fun x => eval x f) univ) (image (fun x => eval x (-g)) univ)
⊢ natDegree f * card (image (fun x => eval x f) univ) + natDegree (-g) * card (image (fun x => eval x (-g)) univ) =
    2 * (card (image (fun x => eval x f) univ) + card (image (fun x => eval x (-g)) univ))
[PROOFSTEP]
simp [natDegree_eq_of_degree_eq_some hf2, natDegree_eq_of_degree_eq_some hg2, mul_add]
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 2
hR : Fintype.card R % 2 = 1
this✝ : DecidableEq R := Classical.decEq R
this : ¬Disjoint (image (fun x => eval x f) univ) (image (fun x => eval x (-g)) univ)
⊢ ∃ a b, eval a f + eval b g = 0
[PROOFSTEP]
simp only [disjoint_left, mem_image] at this 
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 2
hR : Fintype.card R % 2 = 1
this✝ : DecidableEq R := Classical.decEq R
this : ¬∀ ⦃a : R⦄, (∃ a_1, a_1 ∈ univ ∧ eval a_1 f = a) → ¬∃ a_2, a_2 ∈ univ ∧ eval a_2 (-g) = a
⊢ ∃ a b, eval a f + eval b g = 0
[PROOFSTEP]
push_neg at this 
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 2
hR : Fintype.card R % 2 = 1
this✝ : DecidableEq R := Classical.decEq R
this : Exists fun ⦃a⦄ => (∃ a_1, a_1 ∈ univ ∧ eval a_1 f = a) ∧ ∃ a_1, a_1 ∈ univ ∧ eval a_1 (-g) = a
⊢ ∃ a b, eval a f + eval b g = 0
[PROOFSTEP]
rcases this with ⟨x, ⟨a, _, ha⟩, ⟨b, _, hb⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
K : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 2
hR : Fintype.card R % 2 = 1
this : DecidableEq R := Classical.decEq R
x a : R
left✝¹ : a ∈ univ
ha : eval a f = x
b : R
left✝ : b ∈ univ
hb : eval b (-g) = x
⊢ ∃ a b, eval a f + eval b g = 0
[PROOFSTEP]
exact ⟨a, b, by rw [ha, ← hb, eval_neg, neg_add_self]⟩
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype R
f g : R[X]
hf2 : degree f = 2
hg2 : degree g = 2
hR : Fintype.card R % 2 = 1
this : DecidableEq R := Classical.decEq R
x a : R
left✝¹ : a ∈ univ
ha : eval a f = x
b : R
left✝ : b ∈ univ
hb : eval b (-g) = x
⊢ eval a f + eval b g = 0
[PROOFSTEP]
rw [ha, ← hb, eval_neg, neg_add_self]
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
⊢ ∏ x : Kˣ, x = -1
[PROOFSTEP]
classical
have : (∏ x in (@univ Kˣ _).erase (-1), x) = 1 :=
  prod_involution (fun x _ => x⁻¹) (by simp)
    (fun a => by simp (config := { contextual := true }) [Units.inv_eq_self_iff])
    (fun a => by simp [@inv_eq_iff_eq_inv _ _ a]) (by simp)
rw [← insert_erase (mem_univ (-1 : Kˣ)), prod_insert (not_mem_erase _ _), this, mul_one]
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
⊢ ∏ x : Kˣ, x = -1
[PROOFSTEP]
have : (∏ x in (@univ Kˣ _).erase (-1), x) = 1 :=
  prod_involution (fun x _ => x⁻¹) (by simp)
    (fun a => by simp (config := { contextual := true }) [Units.inv_eq_self_iff])
    (fun a => by simp [@inv_eq_iff_eq_inv _ _ a]) (by simp)
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
⊢ ∀ (a : Kˣ) (ha : a ∈ erase univ (-1)), a * (fun x x_1 => x⁻¹) a ha = 1
[PROOFSTEP]
simp
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
a : Kˣ
⊢ ∀ (ha : a ∈ erase univ (-1)), a ≠ 1 → (fun x x_1 => x⁻¹) a ha ≠ a
[PROOFSTEP]
simp (config := { contextual := true }) [Units.inv_eq_self_iff]
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
a : Kˣ
⊢ ∀ (ha : a ∈ erase univ (-1)), (fun x x_1 => x⁻¹) a ha ∈ erase univ (-1)
[PROOFSTEP]
simp [@inv_eq_iff_eq_inv _ _ a]
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
⊢ ∀ (a : Kˣ) (ha : a ∈ erase univ (-1)), (fun x x_1 => x⁻¹) ((fun x x_1 => x⁻¹) a ha) (_ : a⁻¹ ∈ erase univ (-1)) = a
[PROOFSTEP]
simp
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
this : ∏ x in erase univ (-1), x = 1
⊢ ∏ x : Kˣ, x = -1
[PROOFSTEP]
rw [← insert_erase (mem_univ (-1 : Kˣ)), prod_insert (not_mem_erase _ _), this, mul_one]
[GOAL]
K : Type u_1
R : Type u_2
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
ha : a ≠ 0
⊢ a ^ (q - 1) = 1
[PROOFSTEP]
calc
  a ^ (Fintype.card K - 1) = (Units.mk0 a ha ^ (Fintype.card K - 1) : Kˣ).1 := by
    rw [Units.val_pow_eq_pow_val, Units.val_mk0]
  _ = 1 := by
    classical
    rw [← Fintype.card_units, pow_card_eq_one]
    rfl
[GOAL]
K : Type u_1
R : Type u_2
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
ha : a ≠ 0
⊢ a ^ (q - 1) = ↑(Units.mk0 a ha ^ (q - 1))
[PROOFSTEP]
rw [Units.val_pow_eq_pow_val, Units.val_mk0]
[GOAL]
K : Type u_1
R : Type u_2
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
ha : a ≠ 0
⊢ ↑(Units.mk0 a ha ^ (q - 1)) = 1
[PROOFSTEP]
classical
rw [← Fintype.card_units, pow_card_eq_one]
rfl
[GOAL]
K : Type u_1
R : Type u_2
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
ha : a ≠ 0
⊢ ↑(Units.mk0 a ha ^ (q - 1)) = 1
[PROOFSTEP]
rw [← Fintype.card_units, pow_card_eq_one]
[GOAL]
K : Type u_1
R : Type u_2
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
ha : a ≠ 0
⊢ ↑1 = 1
[PROOFSTEP]
rfl
[GOAL]
K : Type u_1
R : Type u_2
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
⊢ a ^ q = a
[PROOFSTEP]
have hp : 0 < Fintype.card K := lt_trans zero_lt_one Fintype.one_lt_card
[GOAL]
K : Type u_1
R : Type u_2
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
hp : 0 < q
⊢ a ^ q = a
[PROOFSTEP]
by_cases h : a = 0
[GOAL]
case pos
K : Type u_1
R : Type u_2
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
hp : 0 < q
h : a = 0
⊢ a ^ q = a
[PROOFSTEP]
rw [h]
[GOAL]
case pos
K : Type u_1
R : Type u_2
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
hp : 0 < q
h : a = 0
⊢ 0 ^ q = 0
[PROOFSTEP]
apply zero_pow hp
[GOAL]
case neg
K : Type u_1
R : Type u_2
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
hp : 0 < q
h : ¬a = 0
⊢ a ^ q = a
[PROOFSTEP]
rw [← Nat.succ_pred_eq_of_pos hp, pow_succ, Nat.pred_eq_sub_one, pow_card_sub_one_eq_one a h, mul_one]
[GOAL]
K : Type u_1
R : Type u_2
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
n : ℕ
a : K
⊢ a ^ q ^ n = a
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
K : Type u_1
R : Type u_2
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
⊢ a ^ q ^ Nat.zero = a
[PROOFSTEP]
simp
[GOAL]
case succ
K : Type u_1
R : Type u_2
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
n : ℕ
ih : a ^ q ^ n = a
⊢ a ^ q ^ Nat.succ n = a
[PROOFSTEP]
simp [pow_succ, pow_mul, ih, pow_card]
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n
[PROOFSTEP]
haveI hp : Fact p.Prime := ⟨CharP.char_is_prime K p⟩
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n
[PROOFSTEP]
letI : Module (ZMod p) K := { (ZMod.castHom dvd_rfl K : ZMod p →+* _).toModule with }
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let src := RingHom.toModule (ZMod.castHom (_ : p ∣ p) K);
  Module.mk (_ : ∀ (r s : ZMod p) (x : K), (r + s) • x = r • x + s • x) (_ : ∀ (x : K), 0 • x = 0)
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n
[PROOFSTEP]
obtain ⟨n, h⟩ := VectorSpace.card_fintype (ZMod p) K
[GOAL]
case intro
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let src := RingHom.toModule (ZMod.castHom (_ : p ∣ p) K);
  Module.mk (_ : ∀ (r s : ZMod p) (x : K), (r + s) • x = r • x + s • x) (_ : ∀ (x : K), 0 • x = 0)
n : ℕ
h : q = Fintype.card (ZMod p) ^ n
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n
[PROOFSTEP]
rw [ZMod.card] at h 
[GOAL]
case intro
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let src := RingHom.toModule (ZMod.castHom (_ : p ∣ p) K);
  Module.mk (_ : ∀ (r s : ZMod p) (x : K), (r + s) • x = r • x + s • x) (_ : ∀ (x : K), 0 • x = 0)
n : ℕ
h : q = p ^ n
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n
[PROOFSTEP]
refine' ⟨⟨n, _⟩, hp.1, h⟩
[GOAL]
case intro
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let src := RingHom.toModule (ZMod.castHom (_ : p ∣ p) K);
  Module.mk (_ : ∀ (r s : ZMod p) (x : K), (r + s) • x = r • x + s • x) (_ : ∀ (x : K), 0 • x = 0)
n : ℕ
h : q = p ^ n
⊢ 0 < n
[PROOFSTEP]
apply Or.resolve_left (Nat.eq_zero_or_pos n)
[GOAL]
case intro
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let src := RingHom.toModule (ZMod.castHom (_ : p ∣ p) K);
  Module.mk (_ : ∀ (r s : ZMod p) (x : K), (r + s) • x = r • x + s • x) (_ : ∀ (x : K), 0 • x = 0)
n : ℕ
h : q = p ^ n
⊢ ¬n = 0
[PROOFSTEP]
rintro rfl
[GOAL]
case intro
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let src := RingHom.toModule (ZMod.castHom (_ : p ∣ p) K);
  Module.mk (_ : ∀ (r s : ZMod p) (x : K), (r + s) • x = r • x + s • x) (_ : ∀ (x : K), 0 • x = 0)
h : q = p ^ 0
⊢ False
[PROOFSTEP]
rw [pow_zero] at h 
[GOAL]
case intro
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let src := RingHom.toModule (ZMod.castHom (_ : p ∣ p) K);
  Module.mk (_ : ∀ (r s : ZMod p) (x : K), (r + s) • x = r • x + s • x) (_ : ∀ (x : K), 0 • x = 0)
h : q = 1
⊢ False
[PROOFSTEP]
have : (0 : K) = 1 := by apply Fintype.card_le_one_iff.mp (le_of_eq h)
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let src := RingHom.toModule (ZMod.castHom (_ : p ∣ p) K);
  Module.mk (_ : ∀ (r s : ZMod p) (x : K), (r + s) • x = r • x + s • x) (_ : ∀ (x : K), 0 • x = 0)
h : q = 1
⊢ 0 = 1
[PROOFSTEP]
apply Fintype.card_le_one_iff.mp (le_of_eq h)
[GOAL]
case intro
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this✝ : Module (ZMod p) K :=
  let src := RingHom.toModule (ZMod.castHom (_ : p ∣ p) K);
  Module.mk (_ : ∀ (r s : ZMod p) (x : K), (r + s) • x = r • x + s • x) (_ : ∀ (x : K), 0 • x = 0)
h : q = 1
this : 0 = 1
⊢ False
[PROOFSTEP]
exact absurd this zero_ne_one
[GOAL]
K : Type u_1
R : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
⊢ ↑q = 0
[PROOFSTEP]
simp
[GOAL]
K : Type u_1
R : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ q - 1 ∣ i
[PROOFSTEP]
classical
obtain ⟨x, hx⟩ := IsCyclic.exists_generator (α := Kˣ)
rw [← Fintype.card_units, ← orderOf_eq_card_of_forall_mem_zpowers hx, orderOf_dvd_iff_pow_eq_one]
constructor
· intro h; apply h
· intro h y
  simp_rw [← mem_powers_iff_mem_zpowers] at hx 
  rcases hx y with ⟨j, rfl⟩
  rw [← pow_mul, mul_comm, pow_mul, h, one_pow]
[GOAL]
K : Type u_1
R : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ q - 1 ∣ i
[PROOFSTEP]
obtain ⟨x, hx⟩ := IsCyclic.exists_generator (α := Kˣ)
[GOAL]
case intro
K : Type u_1
R : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ q - 1 ∣ i
[PROOFSTEP]
rw [← Fintype.card_units, ← orderOf_eq_card_of_forall_mem_zpowers hx, orderOf_dvd_iff_pow_eq_one]
[GOAL]
case intro
K : Type u_1
R : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ x ^ i = 1
[PROOFSTEP]
constructor
[GOAL]
case intro.mp
K : Type u_1
R : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
⊢ (∀ (x : Kˣ), x ^ i = 1) → x ^ i = 1
[PROOFSTEP]
intro h
[GOAL]
case intro.mp
K : Type u_1
R : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
h : ∀ (x : Kˣ), x ^ i = 1
⊢ x ^ i = 1
[PROOFSTEP]
apply h
[GOAL]
case intro.mpr
K : Type u_1
R : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
⊢ x ^ i = 1 → ∀ (x : Kˣ), x ^ i = 1
[PROOFSTEP]
intro h y
[GOAL]
case intro.mpr
K : Type u_1
R : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
h : x ^ i = 1
y : Kˣ
⊢ y ^ i = 1
[PROOFSTEP]
simp_rw [← mem_powers_iff_mem_zpowers] at hx 
[GOAL]
case intro.mpr
K : Type u_1
R : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
h : x ^ i = 1
y : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Submonoid.powers x
⊢ y ^ i = 1
[PROOFSTEP]
rcases hx y with ⟨j, rfl⟩
[GOAL]
case intro.mpr.intro
K : Type u_1
R : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
h : x ^ i = 1
hx : ∀ (x_1 : Kˣ), x_1 ∈ Submonoid.powers x
j : ℕ
⊢ (fun x x_1 => x ^ x_1) x j ^ i = 1
[PROOFSTEP]
rw [← pow_mul, mul_comm, pow_mul, h, one_pow]
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
⊢ ∑ x : Kˣ, ↑(x ^ i) = if q - 1 ∣ i then -1 else 0
[PROOFSTEP]
let φ : Kˣ →* K :=
  { toFun := fun x => x ^ i
    map_one' := by simp
    map_mul' := by intros; simp [mul_pow] }
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
⊢ (fun x => ↑(x ^ i)) 1 = 1
[PROOFSTEP]
simp
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
⊢ ∀ (x y : Kˣ),
    OneHom.toFun { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) } (x * y) =
      OneHom.toFun { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) } x *
        OneHom.toFun { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) } y
[PROOFSTEP]
intros
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
x✝ y✝ : Kˣ
⊢ OneHom.toFun { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) } (x✝ * y✝) =
    OneHom.toFun { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) } x✝ *
      OneHom.toFun { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) } y✝
[PROOFSTEP]
simp [mul_pow]
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
⊢ ∑ x : Kˣ, ↑(x ^ i) = if q - 1 ∣ i then -1 else 0
[PROOFSTEP]
have : Decidable (φ = 1) := by classical infer_instance
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
⊢ Decidable (φ = 1)
[PROOFSTEP]
classical infer_instance
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
⊢ Decidable (φ = 1)
[PROOFSTEP]
infer_instance
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this : Decidable (φ = 1)
⊢ ∑ x : Kˣ, ↑(x ^ i) = if q - 1 ∣ i then -1 else 0
[PROOFSTEP]
calc
  (∑ x : Kˣ, φ x) = if φ = 1 then Fintype.card Kˣ else 0 := sum_hom_units φ
  _ = if q - 1 ∣ i then -1 else 0 :=
    by
    suffices q - 1 ∣ i ↔ φ = 1 by
      simp only [this]
      split_ifs; swap
      · exact Nat.cast_zero
      · rw [Fintype.card_units, Nat.cast_sub, cast_card_eq_zero, Nat.cast_one, zero_sub]
        show 1 ≤ q; exact Fintype.card_pos_iff.mpr ⟨0⟩
    rw [← forall_pow_eq_one_iff, FunLike.ext_iff]
    apply forall_congr'; intro x; simp [Units.ext_iff]
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this : Decidable (φ = 1)
⊢ ↑(if φ = 1 then Fintype.card Kˣ else 0) = if q - 1 ∣ i then -1 else 0
[PROOFSTEP]
suffices q - 1 ∣ i ↔ φ = 1 by
  simp only [this]
  split_ifs; swap
  · exact Nat.cast_zero
  · rw [Fintype.card_units, Nat.cast_sub, cast_card_eq_zero, Nat.cast_one, zero_sub]
    show 1 ≤ q; exact Fintype.card_pos_iff.mpr ⟨0⟩
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
⊢ ↑(if φ = 1 then Fintype.card Kˣ else 0) = if q - 1 ∣ i then -1 else 0
[PROOFSTEP]
simp only [this]
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
⊢ ↑(if
          { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
              map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) } =
            1 then
        Fintype.card Kˣ
      else 0) =
    if
        { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
            map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) } =
          1 then
      -1
    else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ :
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
      map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) } =
    1
⊢ ↑(Fintype.card Kˣ) = -1
case neg
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ :
  ¬{ toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
        map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) } =
      1
⊢ ↑0 = 0
[PROOFSTEP]
swap
[GOAL]
case neg
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ :
  ¬{ toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
        map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) } =
      1
⊢ ↑0 = 0
[PROOFSTEP]
exact Nat.cast_zero
[GOAL]
case pos
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ :
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
      map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) } =
    1
⊢ ↑(Fintype.card Kˣ) = -1
[PROOFSTEP]
rw [Fintype.card_units, Nat.cast_sub, cast_card_eq_zero, Nat.cast_one, zero_sub]
[GOAL]
case pos
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ :
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
      map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) } =
    1
⊢ 1 ≤ q
[PROOFSTEP]
show 1 ≤ q
[GOAL]
case pos
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ :
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
      map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) } =
    1
⊢ 1 ≤ q
[PROOFSTEP]
exact Fintype.card_pos_iff.mpr ⟨0⟩
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this : Decidable (φ = 1)
⊢ q - 1 ∣ i ↔ φ = 1
[PROOFSTEP]
rw [← forall_pow_eq_one_iff, FunLike.ext_iff]
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this : Decidable (φ = 1)
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ ∀ (x : Kˣ), ↑φ x = ↑1 x
[PROOFSTEP]
apply forall_congr'
[GOAL]
case h
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this : Decidable (φ = 1)
⊢ ∀ (a : Kˣ), a ^ i = 1 ↔ ↑φ a = ↑1 a
[PROOFSTEP]
intro x
[GOAL]
case h
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K :=
  { toOneHom := { toFun := fun x => ↑(x ^ i), map_one' := (_ : ↑(1 ^ i) = 1) },
    map_mul' := (_ : ∀ (x y : Kˣ), ↑((x * y) ^ i) = ↑(x ^ i) * ↑(y ^ i)) }
this : Decidable (φ = 1)
x : Kˣ
⊢ x ^ i = 1 ↔ ↑φ x = ↑1 x
[PROOFSTEP]
simp [Units.ext_iff]
[GOAL]
K : Type u_1
R : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
⊢ ∑ x : K, x ^ i = 0
[PROOFSTEP]
by_cases hi : i = 0
[GOAL]
case pos
K : Type u_1
R : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : i = 0
⊢ ∑ x : K, x ^ i = 0
[PROOFSTEP]
simp only [hi, nsmul_one, sum_const, pow_zero, card_univ, cast_card_eq_zero]
[GOAL]
case neg
K : Type u_1
R : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
⊢ ∑ x : K, x ^ i = 0
[PROOFSTEP]
classical
have hiq : ¬q - 1 ∣ i := by contrapose! h; exact Nat.le_of_dvd (Nat.pos_of_ne_zero hi) h
let φ : Kˣ ↪ K := ⟨fun x ↦ x, Units.ext⟩
have : univ.map φ = univ \ {0} := by
  ext x
  simp only [true_and_iff, Function.Embedding.coeFn_mk, mem_sdiff, Units.exists_iff_ne_zero, mem_univ, mem_map,
    exists_prop_of_true, mem_singleton]
calc
  ∑ x : K, x ^ i = ∑ x in univ \ {(0 : K)}, x ^ i := by
    rw [← sum_sdiff ({0} : Finset K).subset_univ, sum_singleton, zero_pow (Nat.pos_of_ne_zero hi), add_zero]
  _ = ∑ x : Kˣ, (x ^ i : K) := by simp [← this, univ.sum_map φ]
  _ = 0 := by rw [sum_pow_units K i, if_neg]; exact hiq
[GOAL]
case neg
K : Type u_1
R : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
⊢ ∑ x : K, x ^ i = 0
[PROOFSTEP]
have hiq : ¬q - 1 ∣ i := by contrapose! h; exact Nat.le_of_dvd (Nat.pos_of_ne_zero hi) h
[GOAL]
K : Type u_1
R : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
⊢ ¬q - 1 ∣ i
[PROOFSTEP]
contrapose! h
[GOAL]
K : Type u_1
R : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
hi : ¬i = 0
h : q - 1 ∣ i
⊢ q - 1 ≤ i
[PROOFSTEP]
exact Nat.le_of_dvd (Nat.pos_of_ne_zero hi) h
[GOAL]
case neg
K : Type u_1
R : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
⊢ ∑ x : K, x ^ i = 0
[PROOFSTEP]
let φ : Kˣ ↪ K := ⟨fun x ↦ x, Units.ext⟩
[GOAL]
case neg
K : Type u_1
R : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x => ↑x, inj' := (_ : Function.Injective Units.val) }
⊢ ∑ x : K, x ^ i = 0
[PROOFSTEP]
have : univ.map φ = univ \ {0} := by
  ext x
  simp only [true_and_iff, Function.Embedding.coeFn_mk, mem_sdiff, Units.exists_iff_ne_zero, mem_univ, mem_map,
    exists_prop_of_true, mem_singleton]
[GOAL]
K : Type u_1
R : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x => ↑x, inj' := (_ : Function.Injective Units.val) }
⊢ map φ univ = univ \ {0}
[PROOFSTEP]
ext x
[GOAL]
case a
K : Type u_1
R : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x => ↑x, inj' := (_ : Function.Injective Units.val) }
x : K
⊢ x ∈ map φ univ ↔ x ∈ univ \ {0}
[PROOFSTEP]
simp only [true_and_iff, Function.Embedding.coeFn_mk, mem_sdiff, Units.exists_iff_ne_zero, mem_univ, mem_map,
  exists_prop_of_true, mem_singleton]
[GOAL]
case neg
K : Type u_1
R : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x => ↑x, inj' := (_ : Function.Injective Units.val) }
this : map φ univ = univ \ {0}
⊢ ∑ x : K, x ^ i = 0
[PROOFSTEP]
calc
  ∑ x : K, x ^ i = ∑ x in univ \ {(0 : K)}, x ^ i := by
    rw [← sum_sdiff ({0} : Finset K).subset_univ, sum_singleton, zero_pow (Nat.pos_of_ne_zero hi), add_zero]
  _ = ∑ x : Kˣ, (x ^ i : K) := by simp [← this, univ.sum_map φ]
  _ = 0 := by rw [sum_pow_units K i, if_neg]; exact hiq
[GOAL]
K : Type u_1
R : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x => ↑x, inj' := (_ : Function.Injective Units.val) }
this : map φ univ = univ \ {0}
⊢ ∑ x : K, x ^ i = ∑ x in univ \ {0}, x ^ i
[PROOFSTEP]
rw [← sum_sdiff ({0} : Finset K).subset_univ, sum_singleton, zero_pow (Nat.pos_of_ne_zero hi), add_zero]
[GOAL]
K : Type u_1
R : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x => ↑x, inj' := (_ : Function.Injective Units.val) }
this : map φ univ = univ \ {0}
⊢ ∑ x in univ \ {0}, x ^ i = ∑ x : Kˣ, ↑(x ^ i)
[PROOFSTEP]
simp [← this, univ.sum_map φ]
[GOAL]
K : Type u_1
R : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x => ↑x, inj' := (_ : Function.Injective Units.val) }
this : map φ univ = univ \ {0}
⊢ ∑ x : Kˣ, ↑(x ^ i) = 0
[PROOFSTEP]
rw [sum_pow_units K i, if_neg]
[GOAL]
case hnc
K : Type u_1
R : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x => ↑x, inj' := (_ : Function.Injective Units.val) }
this : map φ univ = univ \ {0}
⊢ ¬q - 1 ∣ i
[PROOFSTEP]
exact hiq
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
K' : Type u_3
inst✝ : Field K'
p n : ℕ
hp : 1 < p
⊢ natDegree (X ^ p - X) = p
[PROOFSTEP]
have h1 : (X : K'[X]).degree < (X ^ p : K'[X]).degree :=
  by
  rw [degree_X_pow, degree_X]
    -- Porting note: the following line was `exact_mod_cast hp`
  exact WithBot.coe_lt_coe.2 hp
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
K' : Type u_3
inst✝ : Field K'
p n : ℕ
hp : 1 < p
⊢ degree X < degree (X ^ p)
[PROOFSTEP]
rw [degree_X_pow, degree_X]
  -- Porting note: the following line was `exact_mod_cast hp`
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
K' : Type u_3
inst✝ : Field K'
p n : ℕ
hp : 1 < p
⊢ 1 < ↑p
[PROOFSTEP]
exact WithBot.coe_lt_coe.2 hp
[GOAL]
K : Type u_1
R : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
K' : Type u_3
inst✝ : Field K'
p n : ℕ
hp : 1 < p
h1 : degree X < degree (X ^ p)
⊢ natDegree (X ^ p - X) = p
[PROOFSTEP]
rw [natDegree_eq_of_degree_eq (degree_sub_eq_left_of_degree_lt h1), natDegree_X_pow]
[GOAL]
K : Type u_1
R : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
⊢ roots (X ^ q - X) = univ.val
[PROOFSTEP]
classical
have aux : (X ^ q - X : K[X]) ≠ 0 := X_pow_card_sub_X_ne_zero K Fintype.one_lt_card
have : (roots (X ^ q - X : K[X])).toFinset = Finset.univ :=
  by
  rw [eq_univ_iff_forall]
  intro x
  rw [Multiset.mem_toFinset, mem_roots aux, IsRoot.def, eval_sub, eval_pow, eval_X, sub_eq_zero, pow_card]
rw [← this, Multiset.toFinset_val, eq_comm, Multiset.dedup_eq_self]
apply nodup_roots
rw [separable_def]
convert isCoprime_one_right.neg_right (R := K[X]) using 1
rw [derivative_sub, derivative_X, derivative_X_pow, CharP.cast_card_eq_zero K, C_0, zero_mul, zero_sub]
[GOAL]
K : Type u_1
R : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
⊢ roots (X ^ q - X) = univ.val
[PROOFSTEP]
have aux : (X ^ q - X : K[X]) ≠ 0 := X_pow_card_sub_X_ne_zero K Fintype.one_lt_card
[GOAL]
K : Type u_1
R : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
aux : X ^ q - X ≠ 0
⊢ roots (X ^ q - X) = univ.val
[PROOFSTEP]
have : (roots (X ^ q - X : K[X])).toFinset = Finset.univ :=
  by
  rw [eq_univ_iff_forall]
  intro x
  rw [Multiset.mem_toFinset, mem_roots aux, IsRoot.def, eval_sub, eval_pow, eval_X, sub_eq_zero, pow_card]
[GOAL]
K : Type u_1
R : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
aux : X ^ q - X ≠ 0
⊢ Multiset.toFinset (roots (X ^ q - X)) = univ
[PROOFSTEP]
rw [eq_univ_iff_forall]
[GOAL]
K : Type u_1
R : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
aux : X ^ q - X ≠ 0
⊢ ∀ (x : K), x ∈ Multiset.toFinset (roots (X ^ q - X))
[PROOFSTEP]
intro x
[GOAL]
K : Type u_1
R : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
aux : X ^ q - X ≠ 0
x : K
⊢ x ∈ Multiset.toFinset (roots (X ^ q - X))
[PROOFSTEP]
rw [Multiset.mem_toFinset, mem_roots aux, IsRoot.def, eval_sub, eval_pow, eval_X, sub_eq_zero, pow_card]
[GOAL]
K : Type u_1
R : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
aux : X ^ q - X ≠ 0
this : Multiset.toFinset (roots (X ^ q - X)) = univ
⊢ roots (X ^ q - X) = univ.val
[PROOFSTEP]
rw [← this, Multiset.toFinset_val, eq_comm, Multiset.dedup_eq_self]
[GOAL]
K : Type u_1
R : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
aux : X ^ q - X ≠ 0
this : Multiset.toFinset (roots (X ^ q - X)) = univ
⊢ Multiset.Nodup (roots (X ^ q - X))
[PROOFSTEP]
apply nodup_roots
[GOAL]
case hsep
K : Type u_1
R : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
aux : X ^ q - X ≠ 0
this : Multiset.toFinset (roots (X ^ q - X)) = univ
⊢ Separable (X ^ q - X)
[PROOFSTEP]
rw [separable_def]
[GOAL]
case hsep
K : Type u_1
R : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
aux : X ^ q - X ≠ 0
this : Multiset.toFinset (roots (X ^ q - X)) = univ
⊢ IsCoprime (X ^ q - X) (↑derivative (X ^ q - X))
[PROOFSTEP]
convert isCoprime_one_right.neg_right (R := K[X]) using 1
[GOAL]
case h.e'_4
K : Type u_1
R : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
aux : X ^ q - X ≠ 0
this : Multiset.toFinset (roots (X ^ q - X)) = univ
⊢ ↑derivative (X ^ q - X) = -1
[PROOFSTEP]
rw [derivative_sub, derivative_X, derivative_X_pow, CharP.cast_card_eq_zero K, C_0, zero_mul, zero_sub]
[GOAL]
K : Type u_1
R : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Fintype K
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : Algebra (ZMod p✝) K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
hcard : q = p ^ n
⊢ frobenius K p ^ n = 1
[PROOFSTEP]
ext x
[GOAL]
case a
K : Type u_1
R : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Fintype K
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : Algebra (ZMod p✝) K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
hcard : q = p ^ n
x : K
⊢ ↑(frobenius K p ^ n) x = ↑1 x
[PROOFSTEP]
conv_rhs => rw [RingHom.one_def, RingHom.id_apply, ← pow_card x, hcard]
[GOAL]
K : Type u_1
R : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Fintype K
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : Algebra (ZMod p✝) K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
hcard : q = p ^ n
x : K
| ↑1 x
[PROOFSTEP]
rw [RingHom.one_def, RingHom.id_apply, ← pow_card x, hcard]
[GOAL]
K : Type u_1
R : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Fintype K
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : Algebra (ZMod p✝) K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
hcard : q = p ^ n
x : K
| ↑1 x
[PROOFSTEP]
rw [RingHom.one_def, RingHom.id_apply, ← pow_card x, hcard]
[GOAL]
K : Type u_1
R : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Fintype K
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : Algebra (ZMod p✝) K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
hcard : q = p ^ n
x : K
| ↑1 x
[PROOFSTEP]
rw [RingHom.one_def, RingHom.id_apply, ← pow_card x, hcard]
[GOAL]
case a
K : Type u_1
R : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Fintype K
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : Algebra (ZMod p✝) K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
hcard : q = p ^ n
x : K
⊢ ↑(frobenius K p ^ n) x = x ^ p ^ n
[PROOFSTEP]
clear hcard
[GOAL]
case a
K : Type u_1
R : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Fintype K
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : Algebra (ZMod p✝) K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
⊢ ↑(frobenius K p ^ n) x = x ^ p ^ n
[PROOFSTEP]
induction' n with n hn
[GOAL]
case a.zero
K : Type u_1
R : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Fintype K
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : Algebra (ZMod p✝) K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
⊢ ↑(frobenius K p ^ Nat.zero) x = x ^ p ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case a.succ
K : Type u_1
R : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Fintype K
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : Algebra (ZMod p✝) K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
n : ℕ
hn : ↑(frobenius K p ^ n) x = x ^ p ^ n
⊢ ↑(frobenius K p ^ Nat.succ n) x = x ^ p ^ Nat.succ n
[PROOFSTEP]
rw [pow_succ, pow_succ', pow_mul, RingHom.mul_def, RingHom.comp_apply, frobenius_def, hn]
[GOAL]
K : Type u_1
R : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Algebra (ZMod p) K
f : K[X]
⊢ ↑(expand K q) f = f ^ q
[PROOFSTEP]
cases' CharP.exists K with p hp
[GOAL]
case intro
K : Type u_1
R : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
p✝ : ℕ
inst✝¹ : Fact (Nat.Prime p✝)
inst✝ : Algebra (ZMod p✝) K
f : K[X]
p : ℕ
hp : CharP K p
⊢ ↑(expand K q) f = f ^ q
[PROOFSTEP]
letI := hp
[GOAL]
case intro
K : Type u_1
R : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
p✝ : ℕ
inst✝¹ : Fact (Nat.Prime p✝)
inst✝ : Algebra (ZMod p✝) K
f : K[X]
p : ℕ
hp : CharP K p
this : CharP K p := hp
⊢ ↑(expand K q) f = f ^ q
[PROOFSTEP]
rcases FiniteField.card K p with ⟨⟨n, npos⟩, ⟨hp, hn⟩⟩
[GOAL]
case intro.intro.mk.intro
K : Type u_1
R : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
p✝ : ℕ
inst✝¹ : Fact (Nat.Prime p✝)
inst✝ : Algebra (ZMod p✝) K
f : K[X]
p : ℕ
hp✝ : CharP K p
this : CharP K p := hp✝
n : ℕ
npos : 0 < n
hp : Nat.Prime p
hn : q = p ^ ↑{ val := n, property := npos }
⊢ ↑(expand K q) f = f ^ q
[PROOFSTEP]
haveI : Fact p.Prime := ⟨hp⟩
[GOAL]
case intro.intro.mk.intro
K : Type u_1
R : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
p✝ : ℕ
inst✝¹ : Fact (Nat.Prime p✝)
inst✝ : Algebra (ZMod p✝) K
f : K[X]
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
n : ℕ
npos : 0 < n
hp : Nat.Prime p
hn : q = p ^ ↑{ val := n, property := npos }
this : Fact (Nat.Prime p)
⊢ ↑(expand K q) f = f ^ q
[PROOFSTEP]
dsimp at hn 
[GOAL]
case intro.intro.mk.intro
K : Type u_1
R : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
p✝ : ℕ
inst✝¹ : Fact (Nat.Prime p✝)
inst✝ : Algebra (ZMod p✝) K
f : K[X]
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
n : ℕ
npos : 0 < n
hp : Nat.Prime p
hn : q = p ^ n
this : Fact (Nat.Prime p)
⊢ ↑(expand K q) f = f ^ q
[PROOFSTEP]
rw [hn, ← map_expand_pow_char, frobenius_pow hn, RingHom.one_def, map_id]
[GOAL]
K : Type u_1
R : Type u_2
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
⊢ ∃ a b, a ^ 2 + b ^ 2 = x
[PROOFSTEP]
cases' hp.1.eq_two_or_odd with hp2 hp_odd
[GOAL]
case inl
K : Type u_1
R : Type u_2
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp2 : p = 2
⊢ ∃ a b, a ^ 2 + b ^ 2 = x
[PROOFSTEP]
subst p
[GOAL]
case inl
K : Type u_1
R : Type u_2
hp : Fact (Nat.Prime 2)
x : ZMod 2
⊢ ∃ a b, a ^ 2 + b ^ 2 = x
[PROOFSTEP]
change Fin 2 at x 
[GOAL]
case inl
K : Type u_1
R : Type u_2
hp : Fact (Nat.Prime 2)
x : Fin 2
⊢ ∃ a b, a ^ 2 + b ^ 2 = x
[PROOFSTEP]
fin_cases x
[GOAL]
case inl.head
K : Type u_1
R : Type u_2
hp : Fact (Nat.Prime 2)
⊢ ∃ a b, a ^ 2 + b ^ 2 = { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
use 0
[GOAL]
case h
K : Type u_1
R : Type u_2
hp : Fact (Nat.Prime 2)
⊢ ∃ b, 0 ^ 2 + b ^ 2 = { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp
[GOAL]
case inl.tail.head
K : Type u_1
R : Type u_2
hp : Fact (Nat.Prime 2)
⊢ ∃ a b, a ^ 2 + b ^ 2 = { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
use 0, 1
[GOAL]
case h
K : Type u_1
R : Type u_2
hp : Fact (Nat.Prime 2)
⊢ 0 ^ 2 + 1 ^ 2 = { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp
[GOAL]
case inr
K : Type u_1
R : Type u_2
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
⊢ ∃ a b, a ^ 2 + b ^ 2 = x
[PROOFSTEP]
let f : (ZMod p)[X] := X ^ 2
[GOAL]
case inr
K : Type u_1
R : Type u_2
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := X ^ 2
⊢ ∃ a b, a ^ 2 + b ^ 2 = x
[PROOFSTEP]
let g : (ZMod p)[X] := X ^ 2 - C x
[GOAL]
case inr
K : Type u_1
R : Type u_2
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := X ^ 2
g : (ZMod p)[X] := X ^ 2 - ↑C x
⊢ ∃ a b, a ^ 2 + b ^ 2 = x
[PROOFSTEP]
obtain ⟨a, b, hab⟩ : ∃ a b, f.eval a + g.eval b = 0 :=
  @exists_root_sum_quadratic _ _ _ _ f g (degree_X_pow 2) (degree_X_pow_sub_C (by decide) _) (by rw [ZMod.card, hp_odd])
[GOAL]
K : Type u_1
R : Type u_2
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := X ^ 2
g : (ZMod p)[X] := X ^ 2 - ↑C x
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
K : Type u_1
R : Type u_2
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := X ^ 2
g : (ZMod p)[X] := X ^ 2 - ↑C x
⊢ Fintype.card (ZMod p) % 2 = 1
[PROOFSTEP]
rw [ZMod.card, hp_odd]
[GOAL]
case inr.intro.intro
K : Type u_1
R : Type u_2
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := X ^ 2
g : (ZMod p)[X] := X ^ 2 - ↑C x
a b : ZMod p
hab : eval a f + eval b g = 0
⊢ ∃ a b, a ^ 2 + b ^ 2 = x
[PROOFSTEP]
refine' ⟨a, b, _⟩
[GOAL]
case inr.intro.intro
K : Type u_1
R : Type u_2
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := X ^ 2
g : (ZMod p)[X] := X ^ 2 - ↑C x
a b : ZMod p
hab : eval a f + eval b g = 0
⊢ a ^ 2 + b ^ 2 = x
[PROOFSTEP]
rw [← sub_eq_zero]
[GOAL]
case inr.intro.intro
K : Type u_1
R : Type u_2
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := X ^ 2
g : (ZMod p)[X] := X ^ 2 - ↑C x
a b : ZMod p
hab : eval a f + eval b g = 0
⊢ a ^ 2 + b ^ 2 - x = 0
[PROOFSTEP]
simpa only [eval_C, eval_X, eval_pow, eval_sub, ← add_sub_assoc] using hab
[GOAL]
K : Type u_1
R : Type u_2
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
⊢ ∃ a b, a ≤ p / 2 ∧ b ≤ p / 2 ∧ ↑a ^ 2 + ↑b ^ 2 ≡ x [ZMOD ↑p]
[PROOFSTEP]
rcases ZMod.sq_add_sq p x with ⟨a, b, hx⟩
[GOAL]
case intro.intro
K : Type u_1
R : Type u_2
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : a ^ 2 + b ^ 2 = ↑x
⊢ ∃ a b, a ≤ p / 2 ∧ b ≤ p / 2 ∧ ↑a ^ 2 + ↑b ^ 2 ≡ x [ZMOD ↑p]
[PROOFSTEP]
refine ⟨a.valMinAbs.natAbs, b.valMinAbs.natAbs, ZMod.natAbs_valMinAbs_le _, ZMod.natAbs_valMinAbs_le _, ?_⟩
[GOAL]
case intro.intro
K : Type u_1
R : Type u_2
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : a ^ 2 + b ^ 2 = ↑x
⊢ ↑(Int.natAbs (ZMod.valMinAbs a)) ^ 2 + ↑(Int.natAbs (ZMod.valMinAbs b)) ^ 2 ≡ x [ZMOD ↑p]
[PROOFSTEP]
rw [← a.coe_valMinAbs, ← b.coe_valMinAbs] at hx 
[GOAL]
case intro.intro
K : Type u_1
R : Type u_2
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : ↑(ZMod.valMinAbs a) ^ 2 + ↑(ZMod.valMinAbs b) ^ 2 = ↑x
⊢ ↑(Int.natAbs (ZMod.valMinAbs a)) ^ 2 + ↑(Int.natAbs (ZMod.valMinAbs b)) ^ 2 ≡ x [ZMOD ↑p]
[PROOFSTEP]
push_cast
[GOAL]
case intro.intro
K : Type u_1
R : Type u_2
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : ↑(ZMod.valMinAbs a) ^ 2 + ↑(ZMod.valMinAbs b) ^ 2 = ↑x
⊢ |ZMod.valMinAbs a| ^ 2 + |ZMod.valMinAbs b| ^ 2 ≡ x [ZMOD ↑p]
[PROOFSTEP]
rw [sq_abs, sq_abs, ← ZMod.int_cast_eq_int_cast_iff]
[GOAL]
case intro.intro
K : Type u_1
R : Type u_2
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : ↑(ZMod.valMinAbs a) ^ 2 + ↑(ZMod.valMinAbs b) ^ 2 = ↑x
⊢ ↑(ZMod.valMinAbs a ^ 2 + ZMod.valMinAbs b ^ 2) = ↑x
[PROOFSTEP]
exact_mod_cast hx
[GOAL]
K : Type u_1
R : Type u_2
p : ℕ
inst✝ : Fact (Prime p)
x : ℕ
⊢ ∃ a b, a ≤ p / 2 ∧ b ≤ p / 2 ∧ a ^ 2 + b ^ 2 ≡ x [MOD p]
[PROOFSTEP]
simpa only [← Int.coe_nat_modEq_iff] using Nat.sq_add_sq_zmodEq p x
[GOAL]
K : Type u_1
R✝ : Type u_2
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : NeZero p
inst✝ : CharP R p
x : ℤ
⊢ ∃ a b, ↑a ^ 2 + ↑b ^ 2 = ↑x
[PROOFSTEP]
haveI := char_is_prime_of_pos R p
[GOAL]
K : Type u_1
R✝ : Type u_2
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : NeZero p
inst✝ : CharP R p
x : ℤ
this : Fact (Nat.Prime p)
⊢ ∃ a b, ↑a ^ 2 + ↑b ^ 2 = ↑x
[PROOFSTEP]
obtain ⟨a, b, hab⟩ := ZMod.sq_add_sq p x
[GOAL]
case intro.intro
K : Type u_1
R✝ : Type u_2
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : NeZero p
inst✝ : CharP R p
x : ℤ
this : Fact (Nat.Prime p)
a b : ZMod p
hab : a ^ 2 + b ^ 2 = ↑x
⊢ ∃ a b, ↑a ^ 2 + ↑b ^ 2 = ↑x
[PROOFSTEP]
refine' ⟨a.val, b.val, _⟩
[GOAL]
case intro.intro
K : Type u_1
R✝ : Type u_2
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : NeZero p
inst✝ : CharP R p
x : ℤ
this : Fact (Nat.Prime p)
a b : ZMod p
hab : a ^ 2 + b ^ 2 = ↑x
⊢ ↑(ZMod.val a) ^ 2 + ↑(ZMod.val b) ^ 2 = ↑x
[PROOFSTEP]
simpa using congr_arg (ZMod.castHom dvd_rfl R) hab
[GOAL]
K : Type u_1
R : Type u_2
n : ℕ
x : (ZMod n)ˣ
⊢ x ^ φ n = 1
[PROOFSTEP]
cases n
[GOAL]
case zero
K : Type u_1
R : Type u_2
x : (ZMod Nat.zero)ˣ
⊢ x ^ φ Nat.zero = 1
[PROOFSTEP]
rw [Nat.totient_zero, pow_zero]
[GOAL]
case succ
K : Type u_1
R : Type u_2
n✝ : ℕ
x : (ZMod (Nat.succ n✝))ˣ
⊢ x ^ φ (Nat.succ n✝) = 1
[PROOFSTEP]
rw [← card_units_eq_totient, pow_card_eq_one]
[GOAL]
K : Type u_1
R : Type u_2
x n : ℕ
h : coprime x n
⊢ x ^ φ n ≡ 1 [MOD n]
[PROOFSTEP]
rw [← ZMod.eq_iff_modEq_nat]
[GOAL]
K : Type u_1
R : Type u_2
x n : ℕ
h : coprime x n
⊢ ↑(x ^ φ n) = ↑1
[PROOFSTEP]
let x' : Units (ZMod n) := ZMod.unitOfCoprime _ h
[GOAL]
K : Type u_1
R : Type u_2
x n : ℕ
h : coprime x n
x' : (ZMod n)ˣ := unitOfCoprime x h
⊢ ↑(x ^ φ n) = ↑1
[PROOFSTEP]
have := ZMod.pow_totient x'
[GOAL]
K : Type u_1
R : Type u_2
x n : ℕ
h : coprime x n
x' : (ZMod n)ˣ := unitOfCoprime x h
this : x' ^ φ n = 1
⊢ ↑(x ^ φ n) = ↑1
[PROOFSTEP]
apply_fun ((fun (x : Units (ZMod n)) => (x : ZMod n)) : Units (ZMod n) → ZMod n) at this 
[GOAL]
K : Type u_1
R : Type u_2
x n : ℕ
h : coprime x n
x' : (ZMod n)ˣ := unitOfCoprime x h
this : ↑(x' ^ φ n) = ↑1
⊢ ↑(x ^ φ n) = ↑1
[PROOFSTEP]
simpa only [Nat.succ_eq_add_one, Nat.cast_pow, Units.val_one, Nat.cast_one, coe_unitOfCoprime, Units.val_pow_eq_pow_val]
[GOAL]
K : Type u_1
R : Type u_2
V : Type u_3
inst✝⁴ : Fintype K
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Fintype V
⊢ Fintype.card V = q ^ FiniteDimensional.finrank K V
[PROOFSTEP]
let b := IsNoetherian.finsetBasis K V
[GOAL]
K : Type u_1
R : Type u_2
V : Type u_3
inst✝⁴ : Fintype K
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Fintype V
b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K V } K V := IsNoetherian.finsetBasis K V
⊢ Fintype.card V = q ^ FiniteDimensional.finrank K V
[PROOFSTEP]
rw [Module.card_fintype b, ← FiniteDimensional.finrank_eq_card_basis b]
[GOAL]
K : Type u_1
R : Type u_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ZMod p
⊢ x ^ p = x
[PROOFSTEP]
have h := FiniteField.pow_card x
[GOAL]
K : Type u_1
R : Type u_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ZMod p
h : x ^ Fintype.card (ZMod p) = x
⊢ x ^ p = x
[PROOFSTEP]
rwa [ZMod.card p] at h 
[GOAL]
K : Type u_1
R : Type u_2
n p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ZMod p
⊢ x ^ p ^ n = x
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
K : Type u_1
R : Type u_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ZMod p
⊢ x ^ p ^ Nat.zero = x
[PROOFSTEP]
simp
[GOAL]
case succ
K : Type u_1
R : Type u_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ZMod p
n : ℕ
ih : x ^ p ^ n = x
⊢ x ^ p ^ Nat.succ n = x
[PROOFSTEP]
simp [pow_succ, pow_mul, ih, pow_card]
[GOAL]
K : Type u_1
R : Type u_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ frobenius (ZMod p) p = RingHom.id (ZMod p)
[PROOFSTEP]
ext a
[GOAL]
case a
K : Type u_1
R : Type u_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
⊢ ↑(frobenius (ZMod p) p) a = ↑(RingHom.id (ZMod p)) a
[PROOFSTEP]
rw [frobenius_def, ZMod.pow_card, RingHom.id_apply]
[GOAL]
K : Type u_1
R : Type u_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ Fintype.card (ZMod p)ˣ = p - 1
[PROOFSTEP]
rw [Fintype.card_units, card]
[GOAL]
K : Type u_1
R : Type u_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : (ZMod p)ˣ
⊢ a ^ (p - 1) = 1
[PROOFSTEP]
rw [← card_units p, pow_card_eq_one]
[GOAL]
K : Type u_1
R : Type u_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ a ^ (p - 1) = 1
[PROOFSTEP]
have h := FiniteField.pow_card_sub_one_eq_one a ha
[GOAL]
K : Type u_1
R : Type u_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
h : a ^ (Fintype.card (ZMod p) - 1) = 1
⊢ a ^ (p - 1) = 1
[PROOFSTEP]
rwa [ZMod.card p] at h 
[GOAL]
K : Type u_1
R : Type u_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : (ZMod p)[X]
⊢ ↑(expand (ZMod p) p) f = f ^ p
[PROOFSTEP]
have h := FiniteField.expand_card f
[GOAL]
K : Type u_1
R : Type u_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : (ZMod p)[X]
h : ↑(expand (ZMod p) (Fintype.card (ZMod p))) f = f ^ Fintype.card (ZMod p)
⊢ ↑(expand (ZMod p) p) f = f ^ p
[PROOFSTEP]
rwa [ZMod.card p] at h 
[GOAL]
K : Type u_1
R : Type u_2
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n ↑p
⊢ n ^ (p - 1) ≡ 1 [ZMOD ↑p]
[PROOFSTEP]
haveI : Fact p.Prime := ⟨hp⟩
[GOAL]
K : Type u_1
R : Type u_2
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n ↑p
this : Fact (Nat.Prime p)
⊢ n ^ (p - 1) ≡ 1 [ZMOD ↑p]
[PROOFSTEP]
have : ¬(n : ZMod p) = 0 :=
  by
  rw [CharP.int_cast_eq_zero_iff _ p, ← (Nat.prime_iff_prime_int.mp hp).coprime_iff_not_dvd]
  · exact hpn.symm
[GOAL]
K : Type u_1
R : Type u_2
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n ↑p
this : Fact (Nat.Prime p)
⊢ ¬↑n = 0
[PROOFSTEP]
rw [CharP.int_cast_eq_zero_iff _ p, ← (Nat.prime_iff_prime_int.mp hp).coprime_iff_not_dvd]
[GOAL]
K : Type u_1
R : Type u_2
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n ↑p
this : Fact (Nat.Prime p)
⊢ IsCoprime (↑p) n
[PROOFSTEP]
exact hpn.symm
[GOAL]
K : Type u_1
R : Type u_2
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n ↑p
this✝ : Fact (Nat.Prime p)
this : ¬↑n = 0
⊢ n ^ (p - 1) ≡ 1 [ZMOD ↑p]
[PROOFSTEP]
simpa [← ZMod.int_cast_eq_int_cast_iff] using ZMod.pow_card_sub_one_eq_one this
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
⊢ ∃ a, ¬IsSquare a
[PROOFSTEP]
let sq : F → F := fun x => x ^ 2
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
sq : F → F := fun x => x ^ 2
⊢ ∃ a, ¬IsSquare a
[PROOFSTEP]
have h : ¬Function.Injective sq :=
  by
  simp only [Function.Injective, not_forall, exists_prop]
  refine' ⟨-1, 1, _, Ring.neg_one_ne_one_of_char_ne_two hF⟩
  simp only [one_pow, neg_one_sq]
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
sq : F → F := fun x => x ^ 2
⊢ ¬Function.Injective sq
[PROOFSTEP]
simp only [Function.Injective, not_forall, exists_prop]
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
sq : F → F := fun x => x ^ 2
⊢ ∃ x x_1, x ^ 2 = x_1 ^ 2 ∧ ¬x = x_1
[PROOFSTEP]
refine' ⟨-1, 1, _, Ring.neg_one_ne_one_of_char_ne_two hF⟩
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
sq : F → F := fun x => x ^ 2
⊢ (-1) ^ 2 = 1 ^ 2
[PROOFSTEP]
simp only [one_pow, neg_one_sq]
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
sq : F → F := fun x => x ^ 2
h : ¬Function.Injective sq
⊢ ∃ a, ¬IsSquare a
[PROOFSTEP]
rw [Finite.injective_iff_surjective] at h 
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
sq : F → F := fun x => x ^ 2
h : ¬Function.Surjective sq
⊢ ∃ a, ¬IsSquare a
[PROOFSTEP]
simp_rw [IsSquare, ← pow_two, @eq_comm _ _ (_ ^ 2)]
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
sq : F → F := fun x => x ^ 2
h : ¬Function.Surjective sq
⊢ ∃ a, ¬∃ r, r ^ 2 = a
[PROOFSTEP]
unfold Function.Surjective at h 
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
sq : F → F := fun x => x ^ 2
h : ¬∀ (b : F), ∃ a, sq a = b
⊢ ∃ a, ¬∃ r, r ^ 2 = a
[PROOFSTEP]
push_neg at h ⊢
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
sq : F → F := fun x => x ^ 2
h : ∃ b, ∀ (a : F), (fun x => x ^ 2) a ≠ b
⊢ ∃ a, ∀ (r : F), r ^ 2 ≠ a
[PROOFSTEP]
exact h
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
⊢ ringChar F = 2 ↔ Fintype.card F % 2 = 0
[PROOFSTEP]
rcases FiniteField.card F (ringChar F) with ⟨n, hp, h⟩
[GOAL]
case intro.intro
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
⊢ ringChar F = 2 ↔ Fintype.card F % 2 = 0
[PROOFSTEP]
rw [h, Nat.pow_mod]
[GOAL]
case intro.intro
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
⊢ ringChar F = 2 ↔ (ringChar F % 2) ^ ↑n % 2 = 0
[PROOFSTEP]
constructor
[GOAL]
case intro.intro.mp
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
⊢ ringChar F = 2 → (ringChar F % 2) ^ ↑n % 2 = 0
[PROOFSTEP]
intro hF
[GOAL]
case intro.intro.mp
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
hF : ringChar F = 2
⊢ (ringChar F % 2) ^ ↑n % 2 = 0
[PROOFSTEP]
simp [hF]
[GOAL]
case intro.intro.mpr
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
⊢ (ringChar F % 2) ^ ↑n % 2 = 0 → ringChar F = 2
[PROOFSTEP]
rw [← Nat.even_iff, Nat.even_pow]
[GOAL]
case intro.intro.mpr
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
⊢ Even (ringChar F % 2) ∧ ↑n ≠ 0 → ringChar F = 2
[PROOFSTEP]
rintro ⟨hev, hnz⟩
[GOAL]
case intro.intro.mpr.intro
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
hev : Even (ringChar F % 2)
hnz : ↑n ≠ 0
⊢ ringChar F = 2
[PROOFSTEP]
rw [Nat.even_iff, Nat.mod_mod] at hev 
[GOAL]
case intro.intro.mpr.intro
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ ↑n
hev : ringChar F % 2 = 0
hnz : ↑n ≠ 0
⊢ ringChar F = 2
[PROOFSTEP]
exact (Nat.Prime.eq_two_or_odd hp).resolve_right (ne_of_eq_of_ne hev zero_ne_one)
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ a ^ (Fintype.card F / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1
[PROOFSTEP]
have h₁ := FiniteField.pow_card_sub_one_eq_one a ha
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
h₁ : a ^ (Fintype.card F - 1) = 1
⊢ a ^ (Fintype.card F / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1
[PROOFSTEP]
rw [← Nat.two_mul_odd_div_two (FiniteField.odd_card_of_char_ne_two hF), mul_comm, pow_mul, pow_two] at h₁ 
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
h₁ : a ^ (Fintype.card F / 2) * a ^ (Fintype.card F / 2) = 1
⊢ a ^ (Fintype.card F / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1
[PROOFSTEP]
exact mul_self_eq_one_iff.mp h₁
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : Fˣ
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
[PROOFSTEP]
classical
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := Fˣ)
obtain ⟨n, hn⟩ : a ∈ Submonoid.powers g := by rw [mem_powers_iff_mem_zpowers]; apply hg
have hodd := Nat.two_mul_odd_div_two (FiniteField.odd_card_of_char_ne_two hF)
constructor
· rintro ⟨y, rfl⟩
  rw [← pow_two, ← pow_mul, hodd]
  apply_fun Units.val using Units.ext (α := F)
  · push_cast
    exact FiniteField.pow_card_sub_one_eq_one (y : F) (Units.ne_zero y)
· subst a; intro h
  have key : 2 * (Fintype.card F / 2) ∣ n * (Fintype.card F / 2) :=
    by
    rw [← pow_mul] at h 
    rw [hodd, ← Fintype.card_units, ← orderOf_eq_card_of_forall_mem_zpowers hg]
    apply orderOf_dvd_of_pow_eq_one h
  have : 0 < Fintype.card F / 2 := Nat.div_pos Fintype.one_lt_card (by norm_num)
  obtain ⟨m, rfl⟩ := Nat.dvd_of_mul_dvd_mul_right this key
  refine' ⟨g ^ m, _⟩
  dsimp
  rw [mul_comm, pow_mul, pow_two]
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : Fˣ
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
[PROOFSTEP]
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := Fˣ)
[GOAL]
case intro
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
[PROOFSTEP]
obtain ⟨n, hn⟩ : a ∈ Submonoid.powers g := by rw [mem_powers_iff_mem_zpowers]; apply hg
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
⊢ a ∈ Submonoid.powers g
[PROOFSTEP]
rw [mem_powers_iff_mem_zpowers]
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
⊢ a ∈ Subgroup.zpowers g
[PROOFSTEP]
apply hg
[GOAL]
case intro.intro
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hn : (fun x x_1 => x ^ x_1) g n = a
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
[PROOFSTEP]
have hodd := Nat.two_mul_odd_div_two (FiniteField.odd_card_of_char_ne_two hF)
[GOAL]
case intro.intro
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hn : (fun x x_1 => x ^ x_1) g n = a
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
[PROOFSTEP]
constructor
[GOAL]
case intro.intro.mp
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hn : (fun x x_1 => x ^ x_1) g n = a
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
⊢ IsSquare a → a ^ (Fintype.card F / 2) = 1
[PROOFSTEP]
rintro ⟨y, rfl⟩
[GOAL]
case intro.intro.mp.intro
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
y : Fˣ
hn : (fun x x_1 => x ^ x_1) g n = y * y
⊢ (y * y) ^ (Fintype.card F / 2) = 1
[PROOFSTEP]
rw [← pow_two, ← pow_mul, hodd]
[GOAL]
case intro.intro.mp.intro
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
y : Fˣ
hn : (fun x x_1 => x ^ x_1) g n = y * y
⊢ y ^ (Fintype.card F - 1) = 1
[PROOFSTEP]
apply_fun Units.val using Units.ext (α := F)
[GOAL]
case intro.intro.mp.intro
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
y : Fˣ
hn : (fun x x_1 => x ^ x_1) g n = y * y
⊢ ↑(y ^ (Fintype.card F - 1)) = ↑1
[PROOFSTEP]
push_cast
[GOAL]
case intro.intro.mp.intro
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
y : Fˣ
hn : (fun x x_1 => x ^ x_1) g n = y * y
⊢ ↑y ^ (Fintype.card F - 1) = 1
[PROOFSTEP]
exact FiniteField.pow_card_sub_one_eq_one (y : F) (Units.ne_zero y)
[GOAL]
case intro.intro.mpr
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hn : (fun x x_1 => x ^ x_1) g n = a
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
⊢ a ^ (Fintype.card F / 2) = 1 → IsSquare a
[PROOFSTEP]
subst a
[GOAL]
case intro.intro.mpr
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
⊢ (fun x x_1 => x ^ x_1) g n ^ (Fintype.card F / 2) = 1 → IsSquare ((fun x x_1 => x ^ x_1) g n)
[PROOFSTEP]
intro h
[GOAL]
case intro.intro.mpr
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
h : (fun x x_1 => x ^ x_1) g n ^ (Fintype.card F / 2) = 1
⊢ IsSquare ((fun x x_1 => x ^ x_1) g n)
[PROOFSTEP]
have key : 2 * (Fintype.card F / 2) ∣ n * (Fintype.card F / 2) :=
  by
  rw [← pow_mul] at h 
  rw [hodd, ← Fintype.card_units, ← orderOf_eq_card_of_forall_mem_zpowers hg]
  apply orderOf_dvd_of_pow_eq_one h
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
h : (fun x x_1 => x ^ x_1) g n ^ (Fintype.card F / 2) = 1
⊢ 2 * (Fintype.card F / 2) ∣ n * (Fintype.card F / 2)
[PROOFSTEP]
rw [← pow_mul] at h 
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
h : g ^ (n * (Fintype.card F / 2)) = 1
⊢ 2 * (Fintype.card F / 2) ∣ n * (Fintype.card F / 2)
[PROOFSTEP]
rw [hodd, ← Fintype.card_units, ← orderOf_eq_card_of_forall_mem_zpowers hg]
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
h : g ^ (n * (Fintype.card F / 2)) = 1
⊢ orderOf g ∣ n * (Fintype.card F / 2)
[PROOFSTEP]
apply orderOf_dvd_of_pow_eq_one h
[GOAL]
case intro.intro.mpr
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
h : (fun x x_1 => x ^ x_1) g n ^ (Fintype.card F / 2) = 1
key : 2 * (Fintype.card F / 2) ∣ n * (Fintype.card F / 2)
⊢ IsSquare ((fun x x_1 => x ^ x_1) g n)
[PROOFSTEP]
have : 0 < Fintype.card F / 2 := Nat.div_pos Fintype.one_lt_card (by norm_num)
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
h : (fun x x_1 => x ^ x_1) g n ^ (Fintype.card F / 2) = 1
key : 2 * (Fintype.card F / 2) ∣ n * (Fintype.card F / 2)
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
case intro.intro.mpr
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
h : (fun x x_1 => x ^ x_1) g n ^ (Fintype.card F / 2) = 1
key : 2 * (Fintype.card F / 2) ∣ n * (Fintype.card F / 2)
this : 0 < Fintype.card F / 2
⊢ IsSquare ((fun x x_1 => x ^ x_1) g n)
[PROOFSTEP]
obtain ⟨m, rfl⟩ := Nat.dvd_of_mul_dvd_mul_right this key
[GOAL]
case intro.intro.mpr.intro
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
this : 0 < Fintype.card F / 2
m : ℕ
h : (fun x x_1 => x ^ x_1) g (2 * m) ^ (Fintype.card F / 2) = 1
key : 2 * (Fintype.card F / 2) ∣ 2 * m * (Fintype.card F / 2)
⊢ IsSquare ((fun x x_1 => x ^ x_1) g (2 * m))
[PROOFSTEP]
refine' ⟨g ^ m, _⟩
[GOAL]
case intro.intro.mpr.intro
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
this : 0 < Fintype.card F / 2
m : ℕ
h : (fun x x_1 => x ^ x_1) g (2 * m) ^ (Fintype.card F / 2) = 1
key : 2 * (Fintype.card F / 2) ∣ 2 * m * (Fintype.card F / 2)
⊢ (fun x x_1 => x ^ x_1) g (2 * m) = g ^ m * g ^ m
[PROOFSTEP]
dsimp
[GOAL]
case intro.intro.mpr.intro
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
this : 0 < Fintype.card F / 2
m : ℕ
h : (fun x x_1 => x ^ x_1) g (2 * m) ^ (Fintype.card F / 2) = 1
key : 2 * (Fintype.card F / 2) ∣ 2 * m * (Fintype.card F / 2)
⊢ g ^ (2 * m) = g ^ m * g ^ m
[PROOFSTEP]
rw [mul_comm, pow_mul, pow_two]
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
[PROOFSTEP]
apply (iff_congr _ (by simp [Units.ext_iff])).mp (FiniteField.unit_isSquare_iff hF (Units.mk0 a ha))
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ Units.mk0 a ha ^ (Fintype.card F / 2) = 1 ↔ a ^ (Fintype.card F / 2) = 1
[PROOFSTEP]
simp [Units.ext_iff]
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ IsSquare (Units.mk0 a ha) ↔ IsSquare a
[PROOFSTEP]
simp only [IsSquare, Units.ext_iff, Units.val_mk0, Units.val_mul]
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ (∃ r, a = ↑r * ↑r) ↔ ∃ r, a = r * r
[PROOFSTEP]
constructor
[GOAL]
case mp
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ (∃ r, a = ↑r * ↑r) → ∃ r, a = r * r
[PROOFSTEP]
rintro ⟨y, hy⟩
[GOAL]
case mp.intro
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
y : Fˣ
hy : a = ↑y * ↑y
⊢ ∃ r, a = r * r
[PROOFSTEP]
exact ⟨y, hy⟩
[GOAL]
case mpr
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ (∃ r, a = r * r) → ∃ r, a = ↑r * ↑r
[PROOFSTEP]
rintro ⟨y, rfl⟩
[GOAL]
case mpr.intro
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
y : F
ha : y * y ≠ 0
⊢ ∃ r, y * y = ↑r * ↑r
[PROOFSTEP]
have hy : y ≠ 0 := by rintro rfl; simp at ha 
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
y : F
ha : y * y ≠ 0
⊢ y ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
ha : 0 * 0 ≠ 0
⊢ False
[PROOFSTEP]
simp at ha 
[GOAL]
case mpr.intro
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
y : F
ha : y * y ≠ 0
hy : y ≠ 0
⊢ ∃ r, y * y = ↑r * ↑r
[PROOFSTEP]
refine' ⟨Units.mk0 y hy, _⟩
[GOAL]
case mpr.intro
K : Type u_1
R : Type u_2
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
y : F
ha : y * y ≠ 0
hy : y ≠ 0
⊢ y * y = ↑(Units.mk0 y hy) * ↑(Units.mk0 y hy)
[PROOFSTEP]
simp
