docs

leanprover-community · Jul 8, 2024 · 32f3feb · 32f3feb
1 parent 86c2dee
commit 32f3feb
Showing 1 changed file with 2 additions and 1 deletion.
diff --git 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