feat(RingTheory/Flat/Basic): flat modules are torsion-free (#37913)

This PR proves that flat modules are torsion-free.

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/RingTheory/Flat/TorsionFree.lean

@@ -63,6 +63,9 @@ lemma isSMulRegular_of_isRegular {r : R} (hr : IsRegular r) [Flat R M] :
   rw [IsSMulRegular, h2]
   simp [h, LinearEquiv.injective]
 
+instance Module.IsTorsionFree.ofFlat [Flat R M] : IsTorsionFree R M :=
+  ⟨fun _ hr ↦ Module.Flat.isSMulRegular_of_isRegular hr⟩
+
 end Semiring
 
 section Ring