Commit 2024-07-24 08:17 d065779c

View on Github →

chore: fix implicitness of SheafedSpace.ext (#15087)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Scheme.lean

Modified Mathlib/Geometry/RingedSpace/SheafedSpace.lean

modified theorem AlgebraicGeometry.SheafedSpace.ext