Theorem AlgebraicGeometry.Scheme.zeroLocus_mul

Modification history

2026-02-12 15:58

Mathlib/AlgebraicGeometry/Scheme.lean

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

Added AlgebraicGeometry.Scheme.zeroLocus_mul View on Github →