feat(group_theory/perm/cycle): improve doc and namespace for cauchy's…

… theorem (#14471)

Fix a few things in the module docstring, remove namespace, add an additive version and add docstrings for Cauchy's theorem.

https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Existence.20of.20elements.20of.20order.20p.20in.20a.20group/near/284399583

src/group_theory/p_group.lean

@@ -54,7 +54,7 @@ begin
   intros q hq,
   obtain ⟨hq1, hq2⟩ := (nat.mem_factors hG).mp hq,
   haveI : fact q.prime := ⟨hq1⟩,
-  obtain ⟨g, hg⟩ := equiv.perm.exists_prime_order_of_dvd_card q hq2,
+  obtain ⟨g, hg⟩ := exists_prime_order_of_dvd_card q hq2,
   obtain ⟨k, hk⟩ := (iff_order_of.mp h) g,
   exact (hq1.pow_eq_iff.mp (hg.symm.trans hk).symm).1.symm,
 end

src/group_theory/perm/cycle/type.lean

@@ -26,8 +26,8 @@ In this file we define the cycle type of a permutation.
 - `lcm_cycle_type` : The lcm of `σ.cycle_type` equals `order_of σ`
 - `is_conj_iff_cycle_type_eq` : Two permutations are conjugate if and only if they have the same
   cycle type.
-* `exists_prime_order_of_dvd_card`: For every prime `p` dividing the order of a finite group `G`
-  there exists an element of order `p` in `G`. This is known as Cauchy`s theorem.
+- `exists_prime_order_of_dvd_card`: For every prime `p` dividing the order of a finite group `G`
+  there exists an element of order `p` in `G`. This is known as Cauchy's theorem.
 -/
 
 namespace equiv.perm
@@ -461,8 +461,10 @@ subtype.ext (subtype.ext ((congr_arg _ v.1.2.symm).trans v.1.1.rotate_length))
 
 end vectors_prod_eq_one
 
-lemma exists_prime_order_of_dvd_card {G : Type*} [group G] [fintype G] (p : ℕ) [hp : fact p.prime]
-  (hdvd : p ∣ fintype.card G) : ∃ x : G, order_of x = p :=
+/-- For every prime `p` dividing the order of a finite group `G` there exists an element of order
+`p` in `G`. This is known as Cauchy's theorem. -/
+lemma _root_.exists_prime_order_of_dvd_card {G : Type*} [group G] [fintype G] (p : ℕ)
+  [hp : fact p.prime] (hdvd : p ∣ fintype.card G) : ∃ x : G, order_of x = p :=
 begin
   have hp' : p - 1 ≠ 0 := mt tsub_eq_zero_iff_le.mp (not_le_of_lt hp.out.one_lt),
   have Scard := calc p ∣ fintype.card G ^ (p - 1) : hdvd.trans (dvd_pow (dvd_refl _) hp')
@@ -489,6 +491,14 @@ begin
     refl },
 end
 
+/-- For every prime `p` dividing the order of a finite additive group `G` there exists an element of
+order `p` in `G`. This is the additive version of Cauchy's theorem. -/
+lemma _root_.exists_prime_add_order_of_dvd_card {G : Type*} [add_group G] [fintype G] (p : ℕ)
+  [hp : fact p.prime] (hdvd : p ∣ fintype.card G) : ∃ x : G, add_order_of x = p :=
+@exists_prime_order_of_dvd_card (multiplicative G) _ _ _ _ hdvd
+
+attribute [to_additive exists_prime_add_order_of_dvd_card] exists_prime_order_of_dvd_card
+
 end cauchy
 
 lemma subgroup_eq_top_of_swap_mem [decidable_eq α] {H : subgroup (perm α)}