Mathlib v3 is deprecated. Go to Mathlib v4

Theorem algebraic_geometry.is_affine_open.opens_map_from_Spec_basic_open

Modification history

2022-07-17 17:25

src/algebraic_geometry/AffineScheme.lean

feat(algebraic_geometry): Intersection of affine open can be covered by common basic opens (#11649)

Added algebraic_geometry.is_affine_open.opens_map_from_Spec_basic_open View on Github →