diff --git a/Mathlib/RingTheory/Kaehler/CotangentComplex.lean b/Mathlib/RingTheory/Kaehler/CotangentComplex.lean
index dac8656f870a9..ac09d0b46e6e7 100644
--- a/Mathlib/RingTheory/Kaehler/CotangentComplex.lean
+++ b/Mathlib/RingTheory/Kaehler/CotangentComplex.lean
@@ -353,7 +353,8 @@ lemma H1Cotangent.map_comp
     map (g.comp f) = (map g).restrictScalars S ∘ₗ map f := by
   ext; simp [Cotangent.map_comp]
 
-/-- Maps `P₁ → P₂` and `P₂ → P₁` between extensions induce an isomorphism of `H¹(L)`. -/
+/-- Maps `P₁ → P₂` and `P₂ → P₁` between extensions
+induce an isomorphism between `H¹(L_P₁)` and `H¹(L_P₂)`. -/
 @[simps! apply]
 noncomputable
 def H1Cotangent.equiv {P₁ P₂ : Extension R S} (f₁ : P₁.Hom P₂) (f₂ : P₂.Hom P₁) :
diff --git a/Mathlib/RingTheory/Smooth/Kaehler.lean b/Mathlib/RingTheory/Smooth/Kaehler.lean
index b948520724728..fdd183e5bc48a 100644
--- a/Mathlib/RingTheory/Smooth/Kaehler.lean
+++ b/Mathlib/RingTheory/Smooth/Kaehler.lean
@@ -527,7 +527,7 @@ def homInfinitesimal (P₁ P₂ : Extension R S) [FormallySmooth R P₁.Ring] :
       exact FormallySmooth.liftOfSurjective_apply _
             (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring S) _ _ x }
 
-/-- Formally smooth extensions have isomorphic `H¹(L)`. -/
+/-- Formally smooth extensions have isomorphic `H¹(L_P)`. -/
 noncomputable
 def H1Cotangent.equivOfFormallySmooth (P₁ P₂ : Extension R S)
     [FormallySmooth R P₁.Ring] [FormallySmooth R P₂.Ring] :