Def AlgebraicGeometry.Scheme.OpenCover.fromAffineRefinement

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.fromAffineRefinement View on Github →

2024-04-12 14:33

Mathlib/AlgebraicGeometry/OpenImmersion.lean

feat(AlgebraicGeometry/OpenImmersion): Affine open covers, and refinements of open covers by affine ones (#11947)

Added AlgebraicGeometry.Scheme.OpenCover.fromAffineRefinement View on Github →