Def AlgebraicGeometry.Scheme.OpenCover.pullbackCover'

Modification history

2024-06-19 15:38

Mathlib/AlgebraicGeometry/Cover/Open.lean

chore(AlgebraicGeometry/OpenImmersion): Move open covers to its own file. (#13942)

Modified AlgebraicGeometry.Scheme.OpenCover.pullbackCover'View on Github →

2024-05-07 22:42

Mathlib/AlgebraicGeometry/OpenImmersion.lean

perf(BundledCats): more explicit universe annotations (#12741) …

Modified AlgebraicGeometry.Scheme.OpenCover.pullbackCover'View on Github →

2023-11-25 10:19

Mathlib/AlgebraicGeometry/OpenImmersion.lean

feat(AlgebraicGeometry): the big Zariski site (#8549) …

Added AlgebraicGeometry.Scheme.OpenCover.pullbackCover'View on Github →