feat: add theorem cast_subgroup_of_units_card_ne_zero (#6500)

Adds a theorem saying the cardinality of a multiplicative subgroup of a field, cast to the field, is nonzero. As well as `sum_subgroup_units_zero_of_ne_bot` and other theorems about summing over multiplicative subgroups.

Co-authored-by: Pratyush Mishra <prat@upenn.edu>
Co-authored-by:  Buster <rcopley@gmail.com>

Author: BoltonBailey

Mathlib/Data/Fintype/Basic.lean

@@ -1217,13 +1217,18 @@ end Trunc
 
 namespace Multiset
 
-variable [Fintype α] [DecidableEq α]
+variable [Fintype α] [DecidableEq α] [Fintype β]
 
 @[simp]
 theorem count_univ (a : α) : count a Finset.univ.val = 1 :=
   count_eq_one_of_mem Finset.univ.nodup (Finset.mem_univ _)
 #align multiset.count_univ Multiset.count_univ
 
+@[simp]
+theorem map_univ_val_equiv (e : α ≃ β) :
+    map e univ.val = univ.val := by
+  rw [←congr_arg Finset.val (Finset.map_univ_equiv e), Finset.map_val, Equiv.coe_toEmbedding]
+
 end Multiset
 
 /-- Auxiliary definition to show `exists_seq_of_forall_finset_exists`. -/

Mathlib/FieldTheory/Finite/Basic.lean

@@ -111,6 +111,107 @@ theorem prod_univ_units_id_eq_neg_one [CommRing K] [IsDomain K] [Fintype Kˣ] :
     rw [← insert_erase (mem_univ (-1 : Kˣ)), prod_insert (not_mem_erase _ _), this, mul_one]
 #align finite_field.prod_univ_units_id_eq_neg_one FiniteField.prod_univ_units_id_eq_neg_one
 
+theorem card_cast_subgroup_card_ne_zero [Ring K] [NoZeroDivisors K] [Nontrivial K]
+    (G : Subgroup Kˣ) [Fintype G] : (Fintype.card G : K) ≠ 0 := by
+  let n := Fintype.card G
+  intro nzero
+  have ⟨p, char_p⟩ := CharP.exists K
+  have hd : p ∣ n := (CharP.cast_eq_zero_iff K p n).mp nzero
+  cases CharP.char_is_prime_or_zero K p with
+  | inr pzero =>
+    exact (Fintype.card_pos).ne' <| Nat.eq_zero_of_zero_dvd <| pzero ▸ hd
+  | inl pprime =>
+    have fact_pprime := Fact.mk pprime
+    -- G has an element x of order p by Cauchy's theorem
+    have ⟨x, hx⟩ := exists_prime_orderOf_dvd_card p hd
+    -- F has an element u (= ↑↑x) of order p
+    let u := ((x : Kˣ) : K)
+    have hu : orderOf u = p := by rwa [orderOf_units, orderOf_subgroup]
+    -- u ^ p = 1 implies (u - 1) ^ p = 0 and hence u = 1 ...
+    have h : u = 1 := by
+      rw [← sub_left_inj, sub_self 1]
+      apply pow_eq_zero (n := p)
+      rw [sub_pow_char_of_commute, one_pow, ← hu, pow_orderOf_eq_one, sub_self]
+      exact Commute.one_right u
+    -- ... meaning x didn't have order p after all, contradiction
+    apply pprime.one_lt.ne
+    rw [← hu, h, orderOf_one]
+
+/-- The sum of a nontrivial subgroup of the units of a field is zero. -/
+theorem sum_subgroup_units_eq_zero [Ring K] [NoZeroDivisors K]
+    {G : Subgroup Kˣ} [Fintype G] (hg : G ≠ ⊥) :
+    ∑ x : G, (x.val : K) = 0 := by
+  rw [Subgroup.ne_bot_iff_exists_ne_one] at hg
+  rcases hg with ⟨a, ha⟩
+  -- The action of a on G as an embedding
+  let a_mul_emb : G ↪ G := mulLeftEmbedding a
+  -- ... and leaves G unchanged
+  have h_unchanged : Finset.univ.map a_mul_emb = Finset.univ := by simp
+  -- Therefore the sum of x over a G is the sum of a x over G
+  have h_sum_map := Finset.univ.sum_map a_mul_emb fun x => ((x : Kˣ) : K)
+  -- ... and the former is the sum of x over G.
+  -- By algebraic manipulation, we have Σ G, x = ∑ G, a x = a ∑ G, x
+  simp only [h_unchanged, Function.Embedding.coeFn_mk, Function.Embedding.toFun_eq_coe,
+    mulLeftEmbedding_apply, Submonoid.coe_mul, Subgroup.coe_toSubmonoid, Units.val_mul,
+    ← Finset.mul_sum] at h_sum_map
+  -- thus one of (a - 1) or ∑ G, x is zero
+  have hzero : (((a : Kˣ) : K) - 1) = 0 ∨ ∑ x : ↥G, ((x : Kˣ) : K) = 0 := by
+    rw [←mul_eq_zero, sub_mul, ← h_sum_map, one_mul, sub_self]
+  apply Or.resolve_left hzero
+  contrapose! ha
+  ext
+  rwa [←sub_eq_zero]
+
+/-- The sum of a subgroup of the units of a field is 1 if the subgroup is trivial and 1 otherwise -/
+@[simp]
+theorem sum_subgroup_units [Ring K] [NoZeroDivisors K]
+    {G : Subgroup Kˣ} [Fintype G] [Decidable (G = ⊥)] :
+    ∑ x : G, (x.val : K) = if G = ⊥ then 1 else 0 := by
+  by_cases G_bot : G = ⊥
+  · subst G_bot
+    simp only [ite_true, Subgroup.mem_bot, Fintype.card_ofSubsingleton, Nat.cast_ite, Nat.cast_one,
+      Nat.cast_zero, univ_unique, Set.default_coe_singleton, sum_singleton, Units.val_one]
+  · simp only [G_bot, ite_false]
+    exact sum_subgroup_units_eq_zero G_bot
+
+@[simp]
+theorem sum_subgroup_pow_eq_zero [CommRing K] [NoZeroDivisors K]
+    {G : Subgroup Kˣ} [Fintype G] {k : ℕ} (k_pos : k ≠ 0) (k_lt_card_G : k < Fintype.card G) :
+    ∑ x : G, ((x : Kˣ) : K) ^ k = 0 := by
+  nontriviality K
+  have := NoZeroDivisors.to_isDomain K
+  rcases (exists_pow_ne_one_of_isCyclic k_pos k_lt_card_G) with ⟨a, ha⟩
+  rw [Finset.sum_eq_multiset_sum]
+  have h_multiset_map :
+    Finset.univ.val.map (fun x : G => ((x : Kˣ) : K) ^ k) =
+      Finset.univ.val.map (fun x : G => ((x : Kˣ) : K) ^ k * ((a : Kˣ) : K) ^ k) := by
+    simp_rw [← mul_pow]
+    have as_comp :
+      (fun x : ↥G => (((x : Kˣ) : K) * ((a : Kˣ) : K)) ^ k)
+        = (fun x : ↥G => ((x : Kˣ) : K) ^ k) ∘ fun x : ↥G => x * a := by
+      funext x
+      simp only [Function.comp_apply, Submonoid.coe_mul, Subgroup.coe_toSubmonoid, Units.val_mul]
+    rw [as_comp, ← Multiset.map_map]
+    congr
+    rw [eq_comm]
+    exact Multiset.map_univ_val_equiv (Equiv.mulRight a)
+  have h_multiset_map_sum :
+    (Multiset.map (fun x : G => ((x : Kˣ) : K) ^ k) Finset.univ.val).sum =
+      (Multiset.map (fun x : G => ((x : Kˣ) : K) ^ k * ((a : Kˣ) : K) ^ k) Finset.univ.val).sum
+  rw [h_multiset_map]
+  rw [Multiset.sum_map_mul_right] at h_multiset_map_sum
+  have hzero : (((a : Kˣ) : K) ^ k - 1 : K)
+                  * (Multiset.map (fun i : G => (i.val : K) ^ k) Finset.univ.val).sum = 0 := by
+    rw [sub_mul, mul_comm, ← h_multiset_map_sum, one_mul, sub_self]
+  rw [mul_eq_zero] at hzero
+  rcases hzero with h | h
+  · contrapose! ha
+    ext
+    rw [←sub_eq_zero]
+    simp_rw [SubmonoidClass.coe_pow, Units.val_pow_eq_pow_val, OneMemClass.coe_one,
+      Units.val_one, h]
+  · exact h
+
 section
 
 variable [GroupWithZero K] [Fintype K]

Mathlib/GroupTheory/OrderOfElement.lean

@@ -923,6 +923,12 @@ theorem orderOf_eq_card_zpowers : orderOf x = Fintype.card (zpowers x) :=
 #align order_eq_card_zpowers orderOf_eq_card_zpowers
 #align add_order_eq_card_zmultiples addOrderOf_eq_card_zmultiples
 
+@[to_additive card_zmultiples_le]
+theorem card_zpowers_le (a : G) {k : ℕ} (k_pos : k ≠ 0)
+    (ha : a ^ k = 1) : Fintype.card (Subgroup.zpowers a) ≤ k := by
+  rw [← orderOf_eq_card_zpowers]
+  apply orderOf_le_of_pow_eq_one k_pos.bot_lt ha
+
 open QuotientGroup
 
 

Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

@@ -152,6 +152,16 @@ theorem orderOf_eq_card_of_forall_mem_zpowers [Fintype α] {g : α} (hx : ∀ x,
 #align order_of_eq_card_of_forall_mem_zpowers orderOf_eq_card_of_forall_mem_zpowers
 #align add_order_of_eq_card_of_forall_mem_zmultiples addOrderOf_eq_card_of_forall_mem_zmultiples
 
+@[to_additive exists_nsmul_ne_zero_of_isAddCyclic]
+theorem exists_pow_ne_one_of_isCyclic {G : Type*} [Group G] [Fintype G] [G_cyclic : IsCyclic G]
+  {k : ℕ} (k_pos : k ≠ 0) (k_lt_card_G : k < Fintype.card G) : ∃ a : G, a ^ k ≠ 1 := by
+  rcases G_cyclic with ⟨a, ha⟩
+  use a
+  contrapose! k_lt_card_G
+  convert orderOf_le_of_pow_eq_one k_pos.bot_lt k_lt_card_G
+  rw [orderOf_eq_card_zpowers, eq_comm, Subgroup.card_eq_iff_eq_top, eq_top_iff]
+  exact fun x _ ↦ ha x
+
 @[to_additive Infinite.addOrderOf_eq_zero_of_forall_mem_zmultiples]
 theorem Infinite.orderOf_eq_zero_of_forall_mem_zpowers [Infinite α] {g : α}
     (h : ∀ x, x ∈ zpowers g) : orderOf g = 0 := by

Mathlib/GroupTheory/Subgroup/Basic.lean

@@ -932,16 +932,21 @@ theorem nontrivial_iff_exists_ne_one (H : Subgroup G) : Nontrivial H ↔ ∃ x 
 #align subgroup.nontrivial_iff_exists_ne_one Subgroup.nontrivial_iff_exists_ne_one
 #align add_subgroup.nontrivial_iff_exists_ne_zero AddSubgroup.nontrivial_iff_exists_ne_zero
 
+@[to_additive]
+theorem exists_ne_one_of_nontrivial (H : Subgroup G) [Nontrivial H] :
+    ∃ x ∈ H, x ≠ 1 := by
+  rwa [←Subgroup.nontrivial_iff_exists_ne_one]
+
+@[to_additive]
+theorem nontrivial_iff_ne_bot (H : Subgroup G) : Nontrivial H ↔ H ≠ ⊥ := by
+  rw [nontrivial_iff_exists_ne_one, ne_eq, eq_bot_iff_forall]
+  simp only [ne_eq, not_forall, exists_prop]
+
 /-- A subgroup is either the trivial subgroup or nontrivial. -/
 @[to_additive "A subgroup is either the trivial subgroup or nontrivial."]
 theorem bot_or_nontrivial (H : Subgroup G) : H = ⊥ ∨ Nontrivial H := by
-  classical
-    by_cases h : ∀ x ∈ H, x = (1 : G)
-    · left
-      exact H.eq_bot_iff_forall.mpr h
-    · right
-      simp only [not_forall] at h
-      simpa [nontrivial_iff_exists_ne_one] using h
+  have := nontrivial_iff_ne_bot H
+  tauto
 #align subgroup.bot_or_nontrivial Subgroup.bot_or_nontrivial
 #align add_subgroup.bot_or_nontrivial AddSubgroup.bot_or_nontrivial
 
@@ -953,6 +958,11 @@ theorem bot_or_exists_ne_one (H : Subgroup G) : H = ⊥ ∨ ∃ x ∈ H, x ≠ (
 #align subgroup.bot_or_exists_ne_one Subgroup.bot_or_exists_ne_one
 #align add_subgroup.bot_or_exists_ne_zero AddSubgroup.bot_or_exists_ne_zero
 
+@[to_additive]
+lemma ne_bot_iff_exists_ne_one {H : Subgroup G} : H ≠ ⊥ ↔ ∃ a : ↥H, a ≠ 1 := by
+  rw [←nontrivial_iff_ne_bot, nontrivial_iff_exists_ne_one]
+  simp only [ne_eq, Subtype.exists, mk_eq_one_iff, exists_prop]
+
 /-- The inf of two subgroups is their intersection. -/
 @[to_additive "The inf of two `AddSubgroup`s is their intersection."]
 instance : Inf (Subgroup G) :=