refactor(group_theory/order_of_element): now makes sense for infinite…

… monoids (#6587)

This PR generalises `order_of` from finite groups to (potentially infinite) monoids. By convention, the value of `order_of` for an element of infinite order is `0`. This is non-standard for the order of an element, but agrees with the convention that the characteristic of a field is `0` if `1` has infinite additive order. It also enables to remove the assumption `0<n` for some lemmas about orders of elements of the dihedral group, which by convention is also the infinite dihedral group for `n=0`.

The whole file has been restructured to take into account that `order_of` now makes sense for monoids. There is still an open issue about adding [to_additive], but this should be done in a seperate PR. Also, some results could be generalised with assumption `0 < order_of a` instead of finiteness of the whole group.



Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/group_theory/dihedral.lean

@@ -143,7 +143,7 @@ end
 /--
 If `0 < n`, then `sr i` has order 2.
 -/
-@[simp] lemma order_of_sr [fact (0 < n)] (i : zmod n) : order_of (sr i) = 2 :=
+@[simp] lemma order_of_sr (i : zmod n) : order_of (sr i) = 2 :=
 begin
   rw order_of_eq_prime _ _,
   { exact nat.prime_two },
@@ -154,20 +154,40 @@ end
 /--
 If `0 < n`, then `r 1` has order `n`.
 -/
-@[simp] lemma order_of_r_one [hnpos : fact (0 < n)] : order_of (r 1 : dihedral n) = n :=
+@[simp] lemma order_of_r_one : order_of (r 1 : dihedral n) = n :=
 begin
-  cases lt_or_eq_of_le (nat.le_of_dvd hnpos (order_of_dvd_of_pow_eq_one (@r_one_pow_n n))) with h h,
-  { have h1 : (r 1 : dihedral n)^(order_of (r 1)) = 1,
-    { exact pow_order_of_eq_one _ },
-    rw r_one_pow at h1,
-    injection h1 with h2,
-    rw [←zmod.val_eq_zero, zmod.val_nat_cast, nat.mod_eq_of_lt h] at h2,
-    exact absurd h2.symm (ne_of_lt (order_of_pos _)) },
-  { exact h }
+  by_cases hnpos : 0 < n,
+  { haveI : fact (0 < n) := hnpos,
+    cases lt_or_eq_of_le (nat.le_of_dvd hnpos (order_of_dvd_of_pow_eq_one (@r_one_pow_n n)))
+      with h h,
+    { have h1 : (r 1 : dihedral n)^(order_of (r 1)) = 1,
+      { exact pow_order_of_eq_one _ },
+      rw r_one_pow at h1,
+      injection h1 with h2,
+      rw [← zmod.val_eq_zero, zmod.val_nat_cast, nat.mod_eq_of_lt h] at h2,
+      apply absurd h2.symm,
+      apply ne_of_lt,
+      exact absurd h2.symm (ne_of_lt (order_of_pos _)) },
+      { exact h } },
+    { simp only [not_lt, nonpos_iff_eq_zero] at hnpos,
+      rw hnpos,
+      apply order_of_eq_zero,
+      intros m hm,
+      rw [r_one_pow, one_def],
+      by_contradiction,
+      rw not_not at h,
+      have h' : (m : zmod 0) = 0,
+      { exact r.inj h, },
+      have h'' : m = 0,
+      { simp only [int.coe_nat_eq_zero, int.nat_cast_eq_coe_nat] at h',
+        exact h', },
+      rw h'' at hm,
+      apply nat.lt_irrefl,
+      exact hm },
 end
 
 /--
-If `0 < n`, then `i : zmod n` has order `n / gcd n i`
+If `0 < n`, then `i : zmod n` has order `n / gcd n i`.
 -/
 lemma order_of_r [fact (0 < n)] (i : zmod n) : order_of (r i) = n / nat.gcd n i.val :=
 begin