Commit 2025-02-10 21:47 995a19c0

View on Github →

feat(AlgebraicGeometry): vanishing ideal of a subset of scheme (#21434)

Estimated changes

Modified Mathlib/AlgebraicGeometry/IdealSheaf.lean

added theorem AlgebraicGeometry.Scheme.IdealSheafData.gc

added theorem AlgebraicGeometry.Scheme.IdealSheafData.le_radical

added def AlgebraicGeometry.Scheme.IdealSheafData.radical

added theorem AlgebraicGeometry.Scheme.IdealSheafData.radical_bot

added theorem AlgebraicGeometry.Scheme.IdealSheafData.radical_inf

added theorem AlgebraicGeometry.Scheme.IdealSheafData.radical_sup

added theorem AlgebraicGeometry.Scheme.IdealSheafData.radical_top

added theorem AlgebraicGeometry.Scheme.IdealSheafData.subset_support_iff_le_vanishingIdeal

added theorem AlgebraicGeometry.Scheme.IdealSheafData.support_vanishingIdeal

added theorem AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_antimono

added theorem AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_support

added def AlgebraicGeometry.Scheme.nilradical