Theorem CategoryTheory.Pseudofunctor.DescentData.isEquivalence_toDescentData_of_sieve_le

Modification history

2026-02-05 21:16
Mathlib/CategoryTheory/Sites/Descent/Precoverage.lean
feat(CategoryTheory/Sites): characterization of (pre)stacks for a precoverage (#33256) …
Added CategoryTheory.Pseudofunctor.DescentData.isEquivalence_toDescentData_of_sieve_leView on Github →