Theorem AlgebraicGeometry.PresheafedSpace.mk_coe

Modification history

2025-02-05 17:40
Mathlib/Geometry/RingedSpace/PresheafedSpace.lean
chore(PresheafedSpace): remove `mk_coe` and some comments from porting (#21382) …
Deleted AlgebraicGeometry.PresheafedSpace.mk_coeView on Github →
2023-05-21 15:13
Mathlib/AlgebraicGeometry/PresheafedSpace.lean
feat: port AlgebraicGeometry.PresheafedSpace (#4093)
Added AlgebraicGeometry.PresheafedSpace.mk_coeView on Github →