From e47a9a2bcb8e3925634be94d8719bf3e5e08dee6 Mon Sep 17 00:00:00 2001 From: Justus Springer Date: Fri, 22 May 2026 15:13:08 +0100 Subject: [PATCH] fix typo --- Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) 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