Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-01-31 20:42
a0bb6ea9
View on Github →
feat(algebraic_geometry): Open covers of the fibred product. (
#11733
)
Estimated changes
Modified
src/algebraic_geometry/open_immersion.lean
added
def
algebraic_geometry.Scheme.open_cover.copy
added
def
algebraic_geometry.Scheme.open_cover.pushforward_iso
added
def
algebraic_geometry.Scheme.open_cover_of_is_iso
Modified
src/algebraic_geometry/pullbacks.lean
added
def
algebraic_geometry.Scheme.pullback.open_cover_of_base'
added
def
algebraic_geometry.Scheme.pullback.open_cover_of_base
added
def
algebraic_geometry.Scheme.pullback.open_cover_of_left
added
def
algebraic_geometry.Scheme.pullback.open_cover_of_right