Def AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.toFun

Modification history

2023-07-08 03:58

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

feat: port AlgebraicGeometry.ProjectiveSpectrum.Scheme (#5767)

Added AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.toFun View on Github →