Theorem AlgebraicGeometry.Scheme.map_basicOpen'

Modification history

2024-10-24 05:08

Mathlib/AlgebraicGeometry/Restrict.lean

feat(AlgebraicGeometry/Restrict): more API for `Scheme.Opens`. (#17968)

Deleted AlgebraicGeometry.Scheme.map_basicOpen'View on Github →

2024-07-23 21:13

Mathlib/AlgebraicGeometry/Restrict.lean

refactor(AlgebraicGeometry): Introduce `Scheme.Opens`. (#15001) …

Modified AlgebraicGeometry.Scheme.map_basicOpen'View on Github →

2024-06-22 15:35

Mathlib/AlgebraicGeometry/Restrict.lean

refactor(AlgebraicGeometry) Add notation `Γ(X, U)`. (#14025)

Modified AlgebraicGeometry.Scheme.map_basicOpen'View on Github →

2024-05-07 22:42

Mathlib/AlgebraicGeometry/Restrict.lean

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

Modified AlgebraicGeometry.Scheme.map_basicOpen'View on Github →

2023-11-12 21:46

Mathlib/AlgebraicGeometry/Restrict.lean

perf(AlgebraicGeometry): Fix slow and bad proofs (#7747) …

Added AlgebraicGeometry.Scheme.map_basicOpen'View on Github →