Commit 2026-04-28 19:59 ce71d47f
View on Github →chore(AlgebraicGeometry/IdealSheaf): un-private some auxiliary definitions (#38486)
We remove all backward.privateInPublic in the file by removing private from auxiliary definitions. The alternative would be to @[un_expose] the public definitions. This would destroy the def-eq of the underlying type of the induced reduced subscheme structure on some closed subset with the set itself, which is one of the main motivations for including a supportSet field in the definition of AlgebraicGeometry.Scheme.IdealSheafData.