Mathlib v3 is deprecated. Go to Mathlib v4

Def algebraic_geometry.Scheme.affine_basic_open

Modification history

2022-08-05 12:35

src/algebraic_geometry/AffineScheme.lean

feat(algebraic_geometry/open_immersion): Restricting a morphism twice is isomorphic to one restriction. (#15710)

Modified algebraic_geometry.Scheme.affine_basic_open View on Github →

2022-07-22 09:11

src/algebraic_geometry/AffineScheme.lean

feat(algebraic_geometry/AffineScheme): Affine communication lemma (#15487)

Added algebraic_geometry.Scheme.affine_basic_open View on Github →