Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-01-14 10:07
5a6c13bc
View on Github →
feat(algebraic_geometry/open_immersion): Operations on open covers. (
#11442
)
Estimated changes
Modified
src/algebraic_geometry/open_immersion.lean
added
def
algebraic_geometry.Scheme.open_cover.finite_subcover
added
def
algebraic_geometry.Scheme.open_cover.pullback_cover