diff --git a/Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean b/Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean
index 826a96cb9a3f91..e5f0925ac1bd80 100644
--- a/Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean
+++ b/Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean
@@ -325,7 +325,7 @@ lemma IsStandardSmoothOfRelativeDimension.iff_of_isStandardSmooth [Nontrivial S]
   apply Nat.cast_injective (R := Cardinal)
   rwa [← P.rank_kaehlerDifferential]
 
-instance IsStandardSmoothOfRelationDimension.subsingleton_kaehlerDifferential
+instance IsStandardSmoothOfRelativeDimension.subsingleton_kaehlerDifferential
     [IsStandardSmoothOfRelativeDimension 0 R S] : Subsingleton Ω[S⁄R] := by
   cases subsingleton_or_nontrivial S
   · exact Module.subsingleton S _
@@ -333,6 +333,10 @@ instance IsStandardSmoothOfRelationDimension.subsingleton_kaehlerDifferential
   exact Module.subsingleton_of_rank_zero
     (IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential 0)
 
+@[deprecated (since := "2026-05-22")]
+alias IsStandardSmoothOfRelationDimension.subsingleton_kaehlerDifferential :=
+  IsStandardSmoothOfRelativeDimension.subsingleton_kaehlerDifferential
+
 end
 
 instance (priority := 900) [IsStandardSmooth R S] : Smooth R S where