From 32f3feb89adc9581f8d7778e0646e19d78c66e70 Mon Sep 17 00:00:00 2001
From: Jujian Zhang <jujian.zhang1998@outlook.com>
Date: Mon, 8 Jul 2024 05:45:33 +0100
Subject: [PATCH] docs

---
 Mathlib/RingTheory/Flat/CategoryTheory.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/RingTheory/Flat/CategoryTheory.lean b/Mathlib/RingTheory/Flat/CategoryTheory.lean
index 1e15aa970f6c1..f98f8bb8cbe39 100644
--- a/Mathlib/RingTheory/Flat/CategoryTheory.lean
+++ b/Mathlib/RingTheory/Flat/CategoryTheory.lean
@@ -165,7 +165,7 @@ section Tor
 
 open scoped ZeroObject
 
-/-
+/--
 For a flat module `M`, higher tor groups vanish.
 -/
 noncomputable def higherTorIsoZero [Flat R M] (n : ℕ) (N : ModuleCat.{u} R) :
@@ -187,6 +187,7 @@ noncomputable def higherTor'IsoZero [Flat R M] (n : ℕ) (N : ModuleCat.{u} R) :
       rTensor_shortComplex_exact M (pN.complex.sc (n + 1)) (pN.complex_exactAt_succ n))
 
 
+
 end Tor
 
 end Module.Flat