Theorem AlgebraicGeometry.Scheme.pretopology_monotone

Modification history

2026-02-09 11:07

Mathlib/AlgebraicGeometry/Sites/Pretopology.lean

chore(AlgebraicGeometry/Sites): use `Precoverage.toGrothendieck` instead of `Pretopology.toGrothendieck` (#34995) …

Modified AlgebraicGeometry.Scheme.pretopology_monotone View on Github →

2025-10-02 13:49

Mathlib/AlgebraicGeometry/Sites/Pretopology.lean

refactor(AlgebraicGeometry/Sites): redefine pretopologies via precoverages (#29894) …

Added AlgebraicGeometry.Scheme.pretopology_monotone View on Github →