feat(Data): IsScalarTower for ZMod (#30833)

Author: kckennylau

Mathlib/Algebra/Algebra/ZMod.lean

@@ -47,4 +47,23 @@ See note [reducible non-instances]. -/
 abbrev algebra (p : ℕ) [CharP R p] : Algebra (ZMod p) R :=
   algebra' R p dvd_rfl
 
+/-- Any ring with a `ZMod p`-module structure can be upgraded to a `ZMod p`-algebra. Not an
+instance because this is usually not the default way, and this will cause typeclass search loop. -/
+def algebraOfModule (n : ℕ) (R : Type*) [Ring R] [Module (ZMod n) R] : Algebra (ZMod n) R :=
+  Algebra.ofModule' (proof · ·|>.1) (proof · ·|>.2) where
+  proof (r : ZMod n) (x : R) : r • 1 * x = r • x ∧ x * r • 1 = r • x := by
+    obtain _ | n := n
+    · obtain rfl : (inferInstanceAs (Module ℤ R)) = ‹_› := Subsingleton.elim _ _
+      simp [ZMod, Int.cast_comm]
+    · obtain ⟨r, rfl⟩ := ZMod.natCast_zmod_surjective r
+      simp [Nat.cast_smul_eq_nsmul, Nat.cast_comm]
+
+instance instIsScalarTower (n : ℕ) (R M : Type*) [Ring R] [AddCommGroup M]
+    [Module (ZMod n) R] [m₁ : Module (ZMod n) M] [Module R M] :
+    IsScalarTower (ZMod n) R M := by
+  let := ZMod.algebraOfModule n R
+  let m₂ := Module.compHom M (algebraMap (ZMod n) R)
+  obtain rfl : m₁ = m₂ := Subsingleton.elim _ _
+  exact ⟨fun x y z ↦ by rw [Algebra.smul_def, mul_smul]; rfl⟩
+
 end ZMod

Mathlib/Data/ZMod/Basic.lean

@@ -1296,3 +1296,12 @@ def Nat.residueClassesEquiv (N : ℕ) [NeZero N] : ℕ ≃ ZMod N × ℕ where
         cast_id', id_eq, zero_add]
     · simp only [add_comm p.1.val, mul_add_div (NeZero.pos _),
         (Nat.div_eq_zero_iff).2 <| .inr p.1.val_lt, add_zero]
+
+-- there is a faster proof with Module.toAddMonoidEnd
+instance ZMod.instSubsingletonModule (n : ℕ) (M : Type*) [AddCommMonoid M] :
+    Subsingleton (Module (ZMod n) M) := by
+  obtain _ | n := n
+  · exact inferInstanceAs (Subsingleton (Module ℤ M))
+  refine ⟨fun m1 m2 ↦ Module.ext' _ _ fun r m ↦ ?_⟩
+  obtain ⟨r, rfl⟩ := ZMod.natCast_zmod_surjective r
+  rw [(letI := m1; Nat.cast_smul_eq_nsmul _ r m), Nat.cast_smul_eq_nsmul _ r m]