Def 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 →