Theorem AlgebraicGeometry.Scheme.zeroLocus_setMul

Modification history

2026-02-12 15:58

Mathlib/AlgebraicGeometry/Scheme.lean

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

Added AlgebraicGeometry.Scheme.zeroLocus_setMul View on Github →