Mathlib Changelog
v4
Changelog
About
Github
Theorem
AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms
Modification history
2025-05-31 08:21
Mathlib/AlgebraicGeometry/Gluing.lean
chore(AlgebraicGeometry/Gluing): generalize universes in `glueMorphisms` (#25130)
Modified
AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms
View on Github →
2024-11-09 09:38
Mathlib/AlgebraicGeometry/Gluing.lean
refactor(AlgebraicGeometry): replace `OpenCover` by `Cover @IsOpenImmersion` (#18727) …
Added
AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms
View on Github →