From 1d775649ea8e0e1abd5584cd2fe1890edc775880 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Fri, 10 Nov 2023 10:42:44 +0000 Subject: [PATCH] feat: Simple results about `ZMod` (#8205) --- Mathlib/Data/ZMod/Defs.lean | 2 ++ Mathlib/GroupTheory/SpecificGroups/Cyclic.lean | 4 ++++ Mathlib/GroupTheory/Torsion.lean | 8 +++++++- 3 files changed, 13 insertions(+), 1 deletion(-) diff --git a/Mathlib/Data/ZMod/Defs.lean b/Mathlib/Data/ZMod/Defs.lean index dcfa550bef879..d7f089f47ccc4 100644 --- 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 index f070fecf3d77e..1e8d3fec647a6 100644 --- 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 index 6b00ade782798..7c57ead64c95d 100644 --- 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