chore: simplify variables in LinearAlgebra.Dimension.Torsion.Finite (#19839)

Author: Ruben-VandeVelde

Mathlib/LinearAlgebra/Dimension/Torsion/Finite.lean

@@ -11,29 +11,14 @@ import Mathlib.LinearAlgebra.Dimension.Finite
 
 -/
 
-universe u v
+variable {R M : Type*} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M]
 
-variable {R : Type u} {M : Type v}
-variable [Ring R] [AddCommGroup M]
-
-section RankZero
-
-variable [Nontrivial R]
-
-lemma rank_eq_zero_iff_isTorsion {R M} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] :
-    Module.rank R M = 0 ↔ Module.IsTorsion R M := by
+lemma rank_eq_zero_iff_isTorsion: Module.rank R M = 0 ↔ Module.IsTorsion R M := by
   rw [Module.IsTorsion, rank_eq_zero_iff]
   simp [mem_nonZeroDivisors_iff_ne_zero]
 
-end RankZero
-
-section StrongRankCondition
-
 /-- The `StrongRankCondition` is automatic. See `commRing_strongRankCondition`. -/
-theorem Module.finrank_eq_zero_iff_isTorsion {R} [CommRing R] [StrongRankCondition R]
-    [IsDomain R] [Module R M] [Module.Finite R M] :
+theorem Module.finrank_eq_zero_iff_isTorsion [StrongRankCondition R] [Module.Finite R M] :
     finrank R M = 0 ↔ Module.IsTorsion R M := by
   rw [← rank_eq_zero_iff_isTorsion (R := R), ← finrank_eq_rank]
   norm_cast
-
-end StrongRankCondition