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