Commit 2026-03-03 15:46 74706992

View on Github →

feat(CategoryTheory/Sites): topology on Over X is subcanonical if the topology on the base is subcanonical (#36061)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sites/SubcanonicalOver.lean

added theorem CategoryTheory.GrothendieckTopology.subcanonical_over