Theorem AlgebraicGeometry.Scheme.Cover.mem_pretopology

Modification history

2025-10-03 06:19
Mathlib/AlgebraicGeometry/Sites/Pretopology.lean
refactor(AlgebraicGeometry): replace `Scheme.Cover` by an `abbrev` for `ZeroHypercover` (#29061) …
Modified AlgebraicGeometry.Scheme.Cover.mem_pretopologyView on Github →
2025-10-02 13:49
Mathlib/AlgebraicGeometry/Sites/Pretopology.lean
refactor(AlgebraicGeometry/Sites): redefine pretopologies via precoverages (#29894) …
Added AlgebraicGeometry.Scheme.Cover.mem_pretopologyView on Github →