Main results
The main results that the formalization.yaml of FormalFrontier/projective-space lists under status.main_results at commit 9dbd208f, each that the scan finds declared in the file the yaml gives, with its line. They are listed here, not made articles: in several Formal Frontier libraries this list is close to the whole API. The notes are the yaml's.
| Declaration | Kind | Where | Note |
|---|---|---|---|
ProjectiveSpace.polynomialProjToSpec_geometricallyIntegral_of_finite |
theorem | ProjectiveSpace/GeometricallyIntegral.lean, line 341 | |
ProjectiveSpace.polynomialProjToSpec_fin_geometricallyIntegral |
theorem | ProjectiveSpace/GeometricallyIntegral.lean, line 355 | |
AlgebraicGeometry.Proj.isNoetherian |
instance | ProjectiveSpace/Noetherian.lean, line 51 | |
ProjectiveSpace.isNoetherian_polynomialProj |
theorem | ProjectiveSpace/Noetherian.lean, line 79 | |
AlgebraicGeometry.Proj.imageIrrelevant |
def | ProjectiveSpace/DegreeScaledMap.lean, line 44 | |
AlgebraicGeometry.Proj.degreeScaledDomain |
def | ProjectiveSpace/DegreeScaledMap.lean, line 52 | |
AlgebraicGeometry.Proj.degreeScaledDomain_eq_zeroLocus_compl |
theorem | ProjectiveSpace/DegreeScaledMap.lean, line 55 | |
AlgebraicGeometry.Proj.degreeScaledChartMap |
def | ProjectiveSpace/DegreeScaledMap.lean, line 82 | |
AlgebraicGeometry.Proj.degreeScaledChartMap_compatible |
theorem | ProjectiveSpace/DegreeScaledMap.lean, line 263 | |
AlgebraicGeometry.Proj.degreeScaledMap |
def | ProjectiveSpace/DegreeScaledMap.lean, line 288 | |
AlgebraicGeometry.Proj.chartCover_map |
theorem | ProjectiveSpace/DegreeScaledMap.lean, line 296 | |
AlgebraicGeometry.Proj.degreeScaledMap_chartSpec |
theorem | ProjectiveSpace/DegreeScaledMap.lean, line 305 | |
AlgebraicGeometry.Proj.degreeScaledMap_unique |
theorem | ProjectiveSpace/DegreeScaledMap.lean, line 323 | |
AlgebraicGeometry.Proj.degreeZeroRingHom |
def | ProjectiveSpace/DegreeScaledMap.lean, line 332 | |
AlgebraicGeometry.Proj.degreeScaledMap_toSpecZero |
theorem | ProjectiveSpace/DegreeScaledMap.lean, line 374 | |
AlgebraicGeometry.Proj.degreeScaledMap_preimage_basicOpen |
theorem | ProjectiveSpace/DegreeScaledMap.lean, line 472 | |
AlgebraicGeometry.Proj.degreeScaledMap_pointIdeal |
theorem | ProjectiveSpace/DegreeScaledMapPoint.lean, line 139 | |
AlgebraicGeometry.Proj.degreeScaledMap_mem_pointIdeal |
theorem | ProjectiveSpace/DegreeScaledMapPoint.lean, line 167 | |
AlgebraicGeometry.Proj.Veronese.schemeIso |
def | ProjectiveSpace/Veronese.lean, line 291 | |
AlgebraicGeometry.Proj.Veronese.chartEquiv |
def | ProjectiveSpace/Veronese.lean, line 84 | |
AlgebraicGeometry.Proj.Veronese.forward_pointIdeal |
theorem | ProjectiveSpace/Veronese.lean, line 162 | |
AlgebraicGeometry.Proj.Veronese.forward_toSpecZero |
theorem | ProjectiveSpace/Veronese.lean, line 203 | |
AlgebraicGeometry.Proj.map_toSpecZero |
theorem | ProjectiveSpace/GradedProjIso.lean, line 210 | |
GradedRing.Veronese.CoherentTail.TailEquiv.selectedProjIso |
def | ProjectiveSpace/CoherentTailProj.lean, line 41 | |
GradedRing.Veronese.CoherentTail.TailEquiv.projIso |
def | ProjectiveSpace/CoherentTailProj.lean, line 48 | |
GradedRing.Veronese.CoherentTail.TailEquiv.projIso_toSpecZero |
theorem | ProjectiveSpace/CoherentTailProj.lean, line 91 |
Quoted from the main results in formalization.yaml of FormalFrontier/projective-space at commit 9dbd208f, Apache-2.0.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.