lemma Subgroup.prod_top {α β : Type*} [Group α] [Fintype α] [Fintype (⊤ : Subgroup α)]
  [CommMonoid β] (f : α → β) : ∏ x : (⊤ : Subgroup α), f x = ∏ x : α, f x :=
  by simp [Finset.prod_set_coe]

lemma Subgroup.sum_top {α β : Type*} [Group α] [Fintype α] [Fintype (⊤ : Subgroup α)]
  [AddCommMonoid β] (f : α → β) : ∑ x : (⊤ : Subgroup α), f x = ∑ x : α, f x :=
  by simp [Finset.sum_set_coe]

-- how to make these a `to_additive` pair?

lemma prod_units_nonunits {α β : Type*} [Monoid α] [CommMonoid β] [Fintype α] [Fintype αˣ]
  [Fintype <| nonunits α] (f : α → β) :
    (∏ x : αˣ, f x) * ∏ x in (nonunits α).toFinset, f x = ∏ x : α, f x := by
  rw [←Finset.prod_set_coe, ←Fintype.prod_sum_elim]
  apply Fintype.prod_bijective (Sum.elim (· : αˣ → α) (· : nonunits α → α))
  swap; aesop
  refine ⟨?_, fun x ↦ ?_⟩
  · rintro (u | nu) (u | nu) h
    · exact congr(Sum.inl $(Units.ext h))
    · refine (nu.2 ?_).elim
      dsimp at h
      rw [←h]
      exact u.isUnit
    · refine (nu.2 ?_).elim
      dsimp at h
      rw [h]
      exact u.isUnit
    · refine congr(Sum.inr $(Subtype.ext h))
  · by_cases h : IsUnit x
    · exact ⟨.inl h.unit, rfl⟩
    · exact ⟨.inr ⟨x, h⟩, rfl⟩

lemma sum_units_nonunits {α β : Type*} [Monoid α] [AddCommMonoid β] [Fintype α] [Fintype αˣ]
  [Fintype <| nonunits α] (f : α → β) :
    (∑ x : αˣ, f x) + ∑ x in (nonunits α).toFinset, f x = ∑ x : α, f x :=
prod_units_nonunits (β := Multiplicative β) f

-- attribute [to_additive] prod_units_nonunits sum_units_nonunits
-- this is the "correct" additivization but not sure how to tell `to_additive` that

@[simp] lemma nonunits_eq_zero {G : Type*} [GroupWithZero G] : nonunits G = {0} :=
  Set.ext <| fun x ↦ by simpa [nonunits] using (isUnit_iff_ne_zero (a := x)).not

/-- The sum of `x ^ i` as `x` ranges over a finite field of cardinality `q`
is equal to `0` if `i < q - 1`. -/
theorem sum_pow_lt_card_sub_one (i : ℕ) (h : i < q - 1) : ∑ x : K, x ^ i = 0 := by
  by_cases hi : i = 0
  · simp only [hi, nsmul_one, sum_const, pow_zero, card_univ, cast_card_eq_zero]
  classical
  rw [←Fintype.card_units, ←Subgroup.card_top] at h
  have key := sum_subgroup_pow_eq_zero (K := K) (G := ⊤) hi (by convert h)
  erw [Subgroup.sum_top ((· : Kˣ → K) ^ i : Kˣ → K)] at key
  rw [←sum_units_nonunits, ← key]
  simp [hi]

#align finite_field.sum_pow_lt_card_sub_one FiniteField.sum_pow_lt_card_sub_one