Commit 2023-06-29 20:50 2693807d

View on Github →

feat: port AlgebraicGeometry.Limits (#5598)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/Limits.lean

added def AlgebraicGeometry.Scheme.emptyTo

added theorem AlgebraicGeometry.Scheme.empty_ext

added theorem AlgebraicGeometry.Scheme.eq_emptyTo

added theorem AlgebraicGeometry.bot_isAffineOpen

added def AlgebraicGeometry.emptyIsInitial

added theorem AlgebraicGeometry.emptyIsInitial_to