feat: port RingTheory.Kaehler (#4668)

Co-authored-by: ART <anand.rao.art@gmail.com>
Co-authored-by: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com>
Co-authored-by: Bulhwi Cha <chabulhwi@semmalgil.com>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib.lean

@@ -2725,6 +2725,7 @@ import Mathlib.RingTheory.IsAdjoinRoot
 import Mathlib.RingTheory.IsTensorProduct
 import Mathlib.RingTheory.Jacobson
 import Mathlib.RingTheory.JacobsonIdeal
+import Mathlib.RingTheory.Kaehler
 import Mathlib.RingTheory.LaurentSeries
 import Mathlib.RingTheory.LocalProperties
 import Mathlib.RingTheory.Localization.AsSubring

Mathlib/RingTheory/Ideal/Cotangent.lean

@@ -50,13 +50,14 @@ instance Cotangent.moduleOfTower : Module S I.Cotangent :=
   Submodule.Quotient.module' _
 #align ideal.cotangent.module_of_tower Ideal.Cotangent.moduleOfTower
 
-instance : IsScalarTower S S' I.Cotangent := by
+instance Cotangent.isScalarTower : IsScalarTower S S' I.Cotangent := by
   delta Cotangent
   constructor
   intro s s' x
   rw [← @IsScalarTower.algebraMap_smul S' R, ← @IsScalarTower.algebraMap_smul S' R, ← smul_assoc, ←
     IsScalarTower.toAlgHom_apply S S' R, map_smul]
   rfl
+#align ideal.cotangent.is_scalar_tower Ideal.Cotangent.isScalarTower
 
 instance [IsNoetherian R I] : IsNoetherian R I.Cotangent := by delta Cotangent; infer_instance