Theorem TopCat.Presheaf.germ_exist_of_isBasis

Modification history

2025-05-10 07:53
Mathlib/Topology/Sheaves/Stalks.lean
feat(AlgebraicGeometry): equivalence between ideal sheaves and closed subschemes (#24615)
Added TopCat.Presheaf.germ_exist_of_isBasisView on Github →