Commit 2023-06-02 12:18 bbc0ea79

View on Github →

feat: port AlgebraicGeometry.RingedSpace (#4499)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/RingedSpace.lean

added def AlgebraicGeometry.RingedSpace.basicOpen

added theorem AlgebraicGeometry.RingedSpace.basicOpen_le

added theorem AlgebraicGeometry.RingedSpace.basicOpen_mul

added theorem AlgebraicGeometry.RingedSpace.basicOpen_of_isUnit

added theorem AlgebraicGeometry.RingedSpace.basicOpen_res

added theorem AlgebraicGeometry.RingedSpace.basicOpen_res_eq

added theorem AlgebraicGeometry.RingedSpace.isUnit_of_isUnit_germ

added theorem AlgebraicGeometry.RingedSpace.isUnit_res_basicOpen

added theorem AlgebraicGeometry.RingedSpace.isUnit_res_of_isUnit_germ

added theorem AlgebraicGeometry.RingedSpace.mem_basicOpen

added theorem AlgebraicGeometry.RingedSpace.mem_top_basicOpen