Def AlgebraicGeometry.Scheme.OpenCover.restrict

Modification history

2026-05-29 00:22

Mathlib/AlgebraicGeometry/Restrict.lean

refactor(CategoryTheory): redefine `MorphismProperty.IsLocalAtTarget` in terms of presieves (#39978) …

Modified AlgebraicGeometry.Scheme.OpenCover.restrict View on Github →

2024-07-23 19:33

Mathlib/AlgebraicGeometry/Restrict.lean

refactor(AlgebraicGeometry): Introduce `HasRingHomProperty`. (#14992) …

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