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