@[reducible, inline]

abbrev Deformation.IsComplete (A : Type u_2) [CommRing A] [IsLocalRing A] : Prop

Equations

• Deformation.IsComplete A = IsPrecomplete (IsLocalRing.maximalIdeal A) A

instance Deformation.isComplete_of_artinian (A : Type u_2) [CommRing A] [IsLocalRing A] [IsArtinianRing A] : IsComplete A