Mathlib Changelog
Changelog
About
Github
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