Def AlgebraicGeometry.Scheme.IdealSheafData.subschemeFunctor

Modification history

2025-05-12 15:20

Mathlib/AlgebraicGeometry/IdealSheaf.lean

chore(AlgebraicGeometry): split `IdealSheaf.lean` (#24759) …

Modified AlgebraicGeometry.Scheme.IdealSheafData.subschemeFunctor View on Github →

2025-05-10 07:53

Mathlib/AlgebraicGeometry/IdealSheaf.lean

feat(AlgebraicGeometry): equivalence between ideal sheaves and closed subschemes (#24615)

Added AlgebraicGeometry.Scheme.IdealSheafData.subschemeFunctor View on Github →