Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-22 09:11 ac9e3583

View on Github →

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

Estimated changes

Modified src/algebraic_geometry/AffineScheme.lean

added def algebraic_geometry.Scheme.affine_basic_open

added def algebraic_geometry.Scheme.affine_opens

added theorem algebraic_geometry.is_affine_open.basic_open_from_Spec_app

added theorem algebraic_geometry.is_affine_open.basic_open_union_eq_self_iff

added theorem algebraic_geometry.is_affine_open.from_Spec_map_basic_open

added theorem algebraic_geometry.is_affine_open.self_le_basic_open_union_iff

added theorem algebraic_geometry.of_affine_open_cover