Theorem AlgebraicGeometry.Scheme.proetalePrecoverage_le_fpqcPrecoverage

Modification history

2026-03-12 07:50
Mathlib/AlgebraicGeometry/Sites/Proetale.lean
feat(AlgebraicGeometry): `ℓ`-adic cohomology (#36306) …
Added AlgebraicGeometry.Scheme.proetalePrecoverage_le_fpqcPrecoverageView on Github →