Theorem AlgebraicGeometry.RingedSpace.isUnit_res_of_isUnit_germ

Modification history

2024-10-10 07:55
Mathlib/Geometry/RingedSpace/Basic.lean
refactor(Topology/Sheaves): Unbundle `germ`. (#15314)
Modified AlgebraicGeometry.RingedSpace.isUnit_res_of_isUnit_germView on Github →
2023-06-02 12:18
Mathlib/AlgebraicGeometry/RingedSpace.lean
feat: port AlgebraicGeometry.RingedSpace (#4499)
Added AlgebraicGeometry.RingedSpace.isUnit_res_of_isUnit_germView on Github →