feat: Provide glue between AddCommGroup and Module ℤ (#9345)

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Mathlib/Algebra/DirectSum/LinearMap.lean

@@ -17,8 +17,6 @@ domain and codomain.
 
 open Set BigOperators DirectSum
 
-attribute [local instance] Module.free_of_finite_type_torsion_free'
-
 variable {ι R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
   {N : ι → Submodule R M} [DecidableEq ι] (h : IsInternal N)
 

Mathlib/Algebra/Lie/Killing.lean

@@ -54,8 +54,6 @@ variable (R K L M : Type*) [CommRing R] [LieRing L] [LieAlgebra R L]
   [Module.Free R M] [Module.Finite R M]
   [Field K] [LieAlgebra K L] [Module K M] [LieModule K L M] [FiniteDimensional K M]
 
-attribute [local instance] Module.free_of_finite_type_torsion_free'
-
 local notation "φ" => LieModule.toEndomorphism R L M
 
 open LinearMap (trace)

Mathlib/Algebra/Lie/Weights/Linear.lean

@@ -41,8 +41,6 @@ or `R` has characteristic zero.
 
 open Set
 
-attribute [local instance] Module.free_of_finite_type_torsion_free'
-
 variable (R L M : Type*) [CommRing R] [LieRing L] [LieAlgebra R L]
   [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M]
 

Mathlib/Algebra/Module/Submodule/Lattice.lean

@@ -63,6 +63,10 @@ theorem bot_toAddSubmonoid : (⊥ : Submodule R M).toAddSubmonoid = ⊥ :=
   rfl
 #align submodule.bot_to_add_submonoid Submodule.bot_toAddSubmonoid
 
+@[simp]
+lemma bot_toAddSubgroup {R M} [Ring R] [AddCommGroup M] [Module R M] :
+    (⊥ : Submodule R M).toAddSubgroup = ⊥ := rfl
+
 section
 
 variable (R)
@@ -162,6 +166,10 @@ theorem top_toAddSubmonoid : (⊤ : Submodule R M).toAddSubmonoid = ⊤ :=
   rfl
 #align submodule.top_to_add_submonoid Submodule.top_toAddSubmonoid
 
+@[simp]
+lemma top_toAddSubgroup {R M} [Ring R] [AddCommGroup M] [Module R M] :
+    (⊤ : Submodule R M).toAddSubgroup = ⊤ := rfl
+
 @[simp]
 theorem mem_top {x : M} : x ∈ (⊤ : Submodule R M) :=
   trivial

Mathlib/Algebra/Module/Torsion.lean

@@ -720,6 +720,19 @@ theorem noZeroSMulDivisors_iff_torsion_eq_bot : NoZeroSMulDivisors R M ↔ torsi
             exact ⟨⟨a, mem_nonZeroDivisors_of_ne_zero ha⟩, hax⟩ }
 #align submodule.no_zero_smul_divisors_iff_torsion_eq_bot Submodule.noZeroSMulDivisors_iff_torsion_eq_bot
 
+lemma torsion_int {G} [AddCommGroup G] :
+    (torsion ℤ G).toAddSubgroup = AddCommGroup.torsion G := by
+  ext x
+  refine ((isOfFinAddOrder_iff_zsmul_eq_zero (x := x)).trans ?_).symm
+  simp [mem_nonZeroDivisors_iff_ne_zero]
+
+lemma AddMonoid.IsTorsionFree_iff_noZeroSMulDivisors {G : Type*} [AddCommGroup G] :
+    AddMonoid.IsTorsionFree G ↔ NoZeroSMulDivisors ℤ G := by
+  rw [Submodule.noZeroSMulDivisors_iff_torsion_eq_bot,
+    AddMonoid.isTorsionFree_iff_torsion_eq_bot,
+    ← Submodule.toAddSubgroup_injective.eq_iff,
+    Submodule.torsion_int, Submodule.bot_toAddSubgroup]
+
 end Torsion
 
 namespace QuotientTorsion

Mathlib/Algebra/Module/Zlattice.lean

@@ -418,7 +418,7 @@ theorem Zlattice.module_free : Module.Free ℤ L := by
   have : NoZeroSMulDivisors ℤ L := by
     change NoZeroSMulDivisors ℤ (AddSubgroup.toIntSubmodule L)
     exact noZeroSMulDivisors _
-  exact Module.free_of_finite_type_torsion_free'
+  infer_instance
 
 open FiniteDimensional
 

Mathlib/GroupTheory/OrderOfElement.lean

@@ -73,6 +73,16 @@ theorem isOfFinOrder_iff_pow_eq_one : IsOfFinOrder x ↔ ∃ n, 0 < n ∧ x ^ n
 
 @[to_additive] alias ⟨IsOfFinOrder.exists_pow_eq_one, _⟩ := isOfFinOrder_iff_pow_eq_one
 
+@[to_additive]
+lemma isOfFinOrder_iff_zpow_eq_one {G} [Group G] {x : G} :
+    IsOfFinOrder x ↔ ∃ (n : ℤ), n ≠ 0 ∧ x ^ n = 1 := by
+  rw [isOfFinOrder_iff_pow_eq_one]
+  refine ⟨fun ⟨n, hn, hn'⟩ ↦ ⟨n, Int.coe_nat_ne_zero_iff_pos.mpr hn, zpow_coe_nat x n ▸ hn'⟩,
+    fun ⟨n, hn, hn'⟩ ↦ ⟨n.natAbs, Int.natAbs_pos.mpr hn, ?_⟩⟩
+  cases' (Int.natAbs_eq_iff (a := n)).mp rfl with h h;
+  · rwa [h, zpow_coe_nat] at hn'
+  · rwa [h, zpow_neg, inv_eq_one, zpow_coe_nat] at hn'
+
 /-- See also `injective_pow_iff_not_isOfFinOrder`. -/
 @[to_additive "See also `injective_nsmul_iff_not_isOfFinAddOrder`."]
 theorem not_isOfFinOrder_of_injective_pow {x : G} (h : Injective fun n : ℕ => x ^ n) :

Mathlib/GroupTheory/Torsion.lean

@@ -373,6 +373,12 @@ theorem not_isTorsionFree_iff : ¬IsTorsionFree G ↔ ∃ g : G, g ≠ 1 ∧ IsO
 lemma isTorsionFree_of_subsingleton [Subsingleton G] : IsTorsionFree G :=
   fun _a ha _ => ha <| Subsingleton.elim _ _
 
+@[to_additive]
+lemma isTorsionFree_iff_torsion_eq_bot {G} [CommGroup G] :
+    IsTorsionFree G ↔ CommGroup.torsion G = ⊥ := by
+  rw [IsTorsionFree, eq_bot_iff, SetLike.le_def]
+  simp [not_imp_not, CommGroup.mem_torsion]
+
 end Monoid
 
 section Group

Mathlib/LinearAlgebra/FreeModule/PID.lean

@@ -411,14 +411,16 @@ noncomputable def Module.basisOfFiniteTypeTorsionFree' [Module.Finite R M]
   Module.basisOfFiniteTypeTorsionFree Module.Finite.exists_fin.choose_spec.choose_spec
 #align module.basis_of_finite_type_torsion_free' Module.basisOfFiniteTypeTorsionFree'
 
--- It would be nice to make this an instance but it is empirically problematic, possibly because
--- of the loop that it causes with `Module.Free.noZeroSMulDivisors`
-theorem Module.free_of_finite_type_torsion_free' [Module.Finite R M] [NoZeroSMulDivisors R M] :
+instance Module.free_of_finite_type_torsion_free' [Module.Finite R M] [NoZeroSMulDivisors R M] :
     Module.Free R M := by
   obtain ⟨n, b⟩ : Σn, Basis (Fin n) R M := Module.basisOfFiniteTypeTorsionFree'
   exact Module.Free.of_basis b
 #align module.free_of_finite_type_torsion_free' Module.free_of_finite_type_torsion_free'
 
+theorem Module.free_iff_noZeroSMulDivisors [Module.Finite R M] :
+    Module.Free R M ↔ NoZeroSMulDivisors R M :=
+  ⟨fun _ ↦ inferInstance, fun _ ↦ inferInstance⟩
+
 section SmithNormal
 
 /-- A Smith normal form basis for a submodule `N` of a module `M` consists of

Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean

@@ -201,10 +201,10 @@ theorem IsIntegralClosure.isNoetherianRing [IsIntegrallyClosed A] [IsNoetherianR
 and `L` has no zero smul divisors by `A`, the integral closure `C` of `A` in `L` is
 a free `A`-module. -/
 theorem IsIntegralClosure.module_free [NoZeroSMulDivisors A L] [IsPrincipalIdealRing A] :
-    Module.Free A C := by
+    Module.Free A C :=
   haveI : NoZeroSMulDivisors A C := IsIntegralClosure.noZeroSMulDivisors A L
   haveI : IsNoetherian A C := IsIntegralClosure.isNoetherian A K L _
-  exact Module.free_of_finite_type_torsion_free'
+  inferInstance
 #align is_integral_closure.module_free IsIntegralClosure.module_free
 
 /- If `L` is a finite separable extension of `K = Frac(A)`, where `A` is a principal ring