case pos
K : Type u_1
R : Type ?u.640358
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : i = 0
⊢ ∑ x : K, x ^ i = 0

case neg
K : Type u_1
R : Type ?u.640358
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
⊢ ∑ x : K, x ^ i = 0
K : Type u_1
R : Type ?u.640358
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
⊢ ∑ x : K, x ^ i = 0
by_cases hi : i = 0
no goals
case neg
K : Type u_1
R : Type ?u.640358
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
⊢ ∑ x : K, x ^ i = 0
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
no goals
case pos
K : Type u_1
R : Type ?u.640358
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : i = 0
⊢ ∑ x : K, x ^ i = 0
simp only [hi, nsmul_one, sum_const, pow_zero, card_univ, cast_card_eq_zero]
case neg
K : Type u_1
R : Type ?u.640358
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
⊢ ∑ x : K, x ^ i = 0
case neg
K : Type u_1
R : Type ?u.640358
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
⊢ ∑ x : K, x ^ i = 0
have hiq : ¬q - 1 ∣ i := by contrapose! h; exact Nat.le_of_dvd (Nat.pos_of_ne_zero hi) h
case neg
K : Type u_1
R : Type ?u.640358
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
case neg
K : Type u_1
R : Type ?u.640358
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
⊢ ∑ x : K, x ^ i = 0
let φ : Kˣ ↪ K := ⟨fun x ↦ x, Units.ext⟩
case neg
K : Type u_1
R : Type ?u.640358
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
case neg
K : Type u_1
R : Type ?u.640358
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
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]
no goals
case neg
K : Type u_1
R : Type ?u.640358
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
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
K : Type u_1
R : Type ?u.640358
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
hi : ¬i = 0
h : q - 1 ∣ i
⊢ q - 1 ≤ i
K : Type u_1
R : Type ?u.640358
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
⊢ ¬q - 1 ∣ i
contrapose! h
no goals
K : Type u_1
R : Type ?u.640358
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
hi : ¬i = 0
h : q - 1 ∣ i
⊢ q - 1 ≤ i
exact Nat.le_of_dvd (Nat.pos_of_ne_zero hi) h
case a
K : Type u_1
R : Type ?u.640358
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}
K : Type u_1
R : Type ?u.640358
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}
ext x
no goals
case a
K : Type u_1
R : Type ?u.640358
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}
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]
no goals
K : Type u_1
R : Type ?u.640358
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
rw [← sum_sdiff ({0} : Finset K).subset_univ, sum_singleton,
  zero_pow (Nat.pos_of_ne_zero hi), add_zero]
no goals
K : Type u_1
R : Type ?u.640358
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)
simp [← this, univ.sum_map φ]
case hnc
K : Type u_1
R : Type ?u.640358
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
K : Type u_1
R : Type ?u.640358
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
rw [sum_pow_units K i, if_neg]
no goals
case hnc
K : Type u_1
R : Type ?u.640358
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
exact hiq