chore(CategoryTheory/Sites/Descent/Precoverage): deprecate duplicate theorem#41553
Open
tb65536 wants to merge 1 commit into
Open
chore(CategoryTheory/Sites/Descent/Precoverage): deprecate duplicate theorem#41553tb65536 wants to merge 1 commit into
tb65536 wants to merge 1 commit into