refactor(group_theory/order_of_element): Remove fintype hypothesis from pow_coprime (#16989)

This PR removes the `[fintype G]` hypothesis from `pow_coprime (h : coprime (card G) n) : G ≃ G` (the bijection given by the `n`th power map).

Author: tb65536

src/group_theory/order_of_element.lean

@@ -624,7 +624,6 @@ lemma order_eq_card_zpowers : order_of x = fintype.card (zpowers x) :=
 
 open quotient_group
 
-/- TODO: use cardinal theory, introduce `card : set G → ℕ`, or setup decidability for cosets -/
 @[to_additive add_order_of_dvd_card_univ]
 lemma order_of_dvd_card_univ : order_of x ∣ fintype.card G :=
 begin
@@ -649,15 +648,25 @@ begin
           (by rw [eq₁, eq₂, mul_comm])
 end
 
+@[to_additive add_order_of_dvd_nat_card]
+lemma order_of_dvd_nat_card {G : Type*} [group G] {x : G} : order_of x ∣ nat.card G :=
+begin
+  casesI fintype_or_infinite G with h h,
+  { simp only [nat.card_eq_fintype_card, order_of_dvd_card_univ] },
+  { simp only [card_eq_zero_of_infinite, dvd_zero] },
+end
+
+@[simp, to_additive card_nsmul_eq_zero']
+lemma pow_card_eq_one' {G : Type*} [group G] {x : G} : x ^ nat.card G = 1 :=
+order_of_dvd_iff_pow_eq_one.mp order_of_dvd_nat_card
+
 @[simp, to_additive card_nsmul_eq_zero]
 lemma pow_card_eq_one : x ^ fintype.card G = 1 :=
-let ⟨m, hm⟩ := @order_of_dvd_card_univ _ x _ _ in
-by simp [hm, pow_mul, pow_order_of_eq_one]
+by rw [←nat.card_eq_fintype_card, pow_card_eq_one']
 
 @[to_additive] lemma subgroup.pow_index_mem {G : Type*} [group G] (H : subgroup G)
-  [finite (G ⧸ H)] [normal H] (g : G) : g ^ index H ∈ H :=
-by { casesI nonempty_fintype (G ⧸ H),
-  rw [←eq_one_iff, quotient_group.coe_pow H, index_eq_card, pow_card_eq_one] }
+  [normal H] (g : G) : g ^ index H ∈ H :=
+by rw [←eq_one_iff, quotient_group.coe_pow H, index, pow_card_eq_one']
 
 @[to_additive] lemma pow_eq_mod_card (n : ℕ) :
   x ^ n = x ^ (n % fintype.card G) :=
@@ -671,23 +680,23 @@ by rw [zpow_eq_mod_order_of, ← int.mod_mod_of_dvd n (int.coe_nat_dvd.2 order_o
 
 /-- If `gcd(|G|,n)=1` then the `n`th power map is a bijection -/
 @[to_additive "If `gcd(|G|,n)=1` then the smul by `n` is a bijection", simps]
-  def pow_coprime (h : nat.coprime (fintype.card G) n) : G ≃ G :=
+noncomputable def pow_coprime {G : Type*} [group G] (h : (nat.card G).coprime n) : G ≃ G :=
 { to_fun := λ g, g ^ n,
-  inv_fun := λ g, g ^ (nat.gcd_b (fintype.card G) n),
+  inv_fun := λ g, g ^ ((nat.card G).gcd_b n),
   left_inv := λ g, by
-  { have key : g ^ _ = g ^ _ := congr_arg (λ n : ℤ, g ^ n) (nat.gcd_eq_gcd_ab (fintype.card G) n),
+  { have key := congr_arg ((^) g) ((nat.card G).gcd_eq_gcd_ab n),
     rwa [zpow_add, zpow_mul, zpow_mul, zpow_coe_nat, zpow_coe_nat, zpow_coe_nat,
-      h.gcd_eq_one, pow_one, pow_card_eq_one, one_zpow, one_mul, eq_comm] at key },
+      h.gcd_eq_one, pow_one, pow_card_eq_one', one_zpow, one_mul, eq_comm] at key },
   right_inv := λ g, by
-  { have key : g ^ _ = g ^ _ := congr_arg (λ n : ℤ, g ^ n) (nat.gcd_eq_gcd_ab (fintype.card G) n),
+  { have key := congr_arg ((^) g) ((nat.card G).gcd_eq_gcd_ab n),
     rwa [zpow_add, zpow_mul, zpow_mul', zpow_coe_nat, zpow_coe_nat, zpow_coe_nat,
-      h.gcd_eq_one, pow_one, pow_card_eq_one, one_zpow, one_mul, eq_comm] at key } }
+      h.gcd_eq_one, pow_one, pow_card_eq_one', one_zpow, one_mul, eq_comm] at key } }
 
-@[simp, to_additive] lemma pow_coprime_one (h : nat.coprime (fintype.card G) n) :
+@[simp, to_additive] lemma pow_coprime_one {G : Type*} [group G] (h : (nat.card G).coprime n) :
   pow_coprime h 1 = 1 := one_pow n
 
-@[simp, to_additive] lemma pow_coprime_inv (h : nat.coprime (fintype.card G) n) {g : G} :
-  pow_coprime h g⁻¹ = (pow_coprime h g)⁻¹ := inv_pow g n
+@[simp, to_additive] lemma pow_coprime_inv {G : Type*} [group G] (h : (nat.card G).coprime n)
+  {g : G} : pow_coprime h g⁻¹ = (pow_coprime h g)⁻¹ := inv_pow g n
 
 @[to_additive add_inf_eq_bot_of_coprime]
 lemma inf_eq_bot_of_coprime {G : Type*} [group G] {H K : subgroup G} [fintype H] [fintype K]

src/group_theory/schur_zassenhaus.lean

@@ -78,29 +78,27 @@ begin
   exact self_eq_mul_right.mpr ((quotient_group.eq_one_iff _).mpr h.2),
 end
 
-variables [fintype H]
-
-lemma eq_one_of_smul_eq_one (hH : nat.coprime (fintype.card H) H.index)
+lemma eq_one_of_smul_eq_one (hH : nat.coprime (nat.card H) H.index)
   (α : H.quotient_diff) (h : H) : h • α = α → h = 1 :=
 quotient.induction_on' α $ λ α hα, (pow_coprime hH).injective $
   calc h ^ H.index = diff (monoid_hom.id H) ((op ((h⁻¹ : H) : G)) • α) α :
     by rw [←diff_inv, smul_diff', diff_self, one_mul, inv_pow, inv_inv]
   ... = 1 ^ H.index : (quotient.exact' hα).trans (one_pow H.index).symm
 
-lemma exists_smul_eq (hH : nat.coprime (fintype.card H) H.index)
+lemma exists_smul_eq (hH : nat.coprime (nat.card H) H.index)
   (α β : H.quotient_diff) : ∃ h : H, h • α = β :=
 quotient.induction_on' α (quotient.induction_on' β (λ β α, exists_imp_exists (λ n, quotient.sound')
   ⟨(pow_coprime hH).symm (diff (monoid_hom.id H) β α), (diff_inv _ _ _).symm.trans
   (inv_eq_one.mpr ((smul_diff' β α ((pow_coprime hH).symm (diff (monoid_hom.id H) β α))⁻¹).trans
   (by rw [inv_pow, ←pow_coprime_apply hH, equiv.apply_symm_apply, mul_inv_self])))⟩))
 
 lemma is_complement'_stabilizer_of_coprime {α : H.quotient_diff}
-  (hH : nat.coprime (fintype.card H) H.index) : is_complement' H (stabilizer G α) :=
+  (hH : nat.coprime (nat.card H) H.index) : is_complement' H (stabilizer G α) :=
 is_complement'_stabilizer α (eq_one_of_smul_eq_one hH α) (λ g, exists_smul_eq hH (g • α) α)
 
 /-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime` -/
 private lemma exists_right_complement'_of_coprime_aux
-  (hH : nat.coprime (fintype.card H) H.index) : ∃ K : subgroup G, is_complement' H K :=
+  (hH : nat.coprime (nat.card H) H.index) : ∃ K : subgroup G, is_complement' H K :=
 nonempty_of_inhabited.elim (λ α, ⟨stabilizer G α, is_complement'_stabilizer_of_coprime hH⟩)
 
 end schur_zassenhaus_abelian
@@ -256,6 +254,7 @@ begin
   refine not_forall_not.mp (λ h3, _),
   haveI := by exactI
     schur_zassenhaus_induction.step7 hN (λ G' _ _ hG', by { apply ih _ hG', refl }) h3,
+  rw ← nat.card_eq_fintype_card at hN,
   exact not_exists_of_forall_not h3 (exists_right_complement'_of_coprime_aux hN),
 end