feat: Simple results about ZMod (#8205)

leanprover-community · Nov 10, 2023 · 1d77564 · 1d77564
1 parent e72b701
commit 1d77564
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 1 deletion.
diff --git a/Mathlib/Data/ZMod/Defs.lean b/Mathlib/Data/ZMod/Defs.lean
@@ -108,6 +108,8 @@ instance ZMod.repr : ∀ n : ℕ, Repr (ZMod n)
 
 namespace ZMod
 
+instance instUnique : Unique (ZMod 1) := Fin.unique
+
 instance fintype : ∀ (n : ℕ) [NeZero n], Fintype (ZMod n)
   | 0, h => (h.ne rfl).elim
   | n + 1, _ => Fin.fintype (n + 1)

diff --git a/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean b/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
@@ -605,6 +605,10 @@ theorem IsCyclic.exponent_eq_zero_of_infinite [Group α] [IsCyclic α] [Infinite
 instance ZMod.instIsAddCyclic (n : ℕ) : IsAddCyclic (ZMod n) where
   exists_generator := ⟨1, fun n ↦ ⟨n, by simp⟩⟩
 
+instance ZMod.instIsSimpleAddGroup {p : ℕ} [Fact p.Prime] : IsSimpleAddGroup (ZMod p) :=
+  AddCommGroup.is_simple_iff_isAddCyclic_and_prime_card.2
+    ⟨by infer_instance, by simpa using (Fact.out : p.Prime)⟩
+
 @[simp]
 protected theorem ZMod.exponent (n : ℕ) : AddMonoid.exponent (ZMod n) = n := by
   cases n

diff --git a/Mathlib/GroupTheory/Torsion.lean b/Mathlib/GroupTheory/Torsion.lean
@@ -361,6 +361,8 @@ def IsTorsionFree :=
 #align monoid.is_torsion_free Monoid.IsTorsionFree
 #align add_monoid.is_torsion_free AddMonoid.IsTorsionFree
 
+variable {G}
+
 /-- A nontrivial monoid is not torsion-free if any nontrivial element has finite order. -/
 @[to_additive (attr := simp) "An additive monoid is not torsion free if any
   nontrivial element has finite order."]
@@ -369,6 +371,10 @@ theorem not_isTorsionFree_iff : ¬IsTorsionFree G ↔ ∃ g : G, g ≠ 1 ∧ IsO
 #align monoid.not_is_torsion_free_iff Monoid.not_isTorsionFree_iff
 #align add_monoid.not_is_torsion_free_iff AddMonoid.not_isTorsionFree_iff
 
+@[to_additive (attr := simp)]
+lemma isTorsionFree_of_subsingleton [Subsingleton G] : IsTorsionFree G :=
+  fun _a ha _ => ha <| Subsingleton.elim _ _
+
 end Monoid
 
 section Group
@@ -381,7 +387,7 @@ variable [Group G]
 @[to_additive AddMonoid.IsTorsion.not_torsion_free
       "A nontrivial additive torsion group is not torsion-free."]
 theorem IsTorsion.not_torsion_free [hN : Nontrivial G] : IsTorsion G → ¬IsTorsionFree G := fun tG =>
-  (not_isTorsionFree_iff _).mpr <| by
+  not_isTorsionFree_iff.mpr <| by
     obtain ⟨x, hx⟩ := (nontrivial_iff_exists_ne (1 : G)).mp hN
     exact ⟨x, hx, tG x⟩
 #align is_torsion.not_torsion_free IsTorsion.not_torsion_free