Theorem CategoryTheory.Precoverage.le_toPrecoverage_toGrothendieck

Modification history

2026-03-03 16:04
Mathlib/CategoryTheory/Sites/PrecoverageToGrothendieck.lean
chore(CategoryTheory/Sites): generalize `Precoverage.toGrothendieck_le_iff_le_toPrecoverage` (#35920)
Added CategoryTheory.Precoverage.le_toPrecoverage_toGrothendieckView on Github →