Commit 2026-02-12 15:58 fe7639f2

View on Github →

feat(AlgebraicGeometry): Semiring structure on ideal sheaves (#34935)

Estimated changes

Modified Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean

added theorem AlgebraicGeometry.Scheme.IdealSheafData.add_eq_sup

added theorem AlgebraicGeometry.Scheme.IdealSheafData.bot_mul

modified def AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine

added theorem AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_apply

added theorem AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_symm_apply

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_mul

added theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_pow

added theorem AlgebraicGeometry.Scheme.IdealSheafData.inf_mul

added theorem AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff_mem_support

added theorem AlgebraicGeometry.Scheme.IdealSheafData.mul_bot

added theorem AlgebraicGeometry.Scheme.IdealSheafData.mul_inf

added theorem AlgebraicGeometry.Scheme.IdealSheafData.mul_top

added theorem AlgebraicGeometry.Scheme.IdealSheafData.one_eq_top

added theorem AlgebraicGeometry.Scheme.IdealSheafData.radical_mul

added theorem AlgebraicGeometry.Scheme.IdealSheafData.support_mul

added theorem AlgebraicGeometry.Scheme.IdealSheafData.support_pow

added theorem AlgebraicGeometry.Scheme.IdealSheafData.support_pow_succ

added theorem AlgebraicGeometry.Scheme.IdealSheafData.top_mul

added theorem AlgebraicGeometry.Scheme.IdealSheafData.zero_eq_bot

Modified Mathlib/AlgebraicGeometry/Scheme.lean

added theorem AlgebraicGeometry.Scheme.zeroLocus_mul

added theorem AlgebraicGeometry.Scheme.zeroLocus_setMul