OAI/NumberTheory/PiExponent/Geometry/ProjectiveSpaceSerre.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.PiExponent.ProjectiveO1.schemeUnitline 14 - theorem
OAI.PiExponent.ProjectiveO1.standardPower_ext_eq_zeroline 20 - theorem
OAI.PiExponent.ProjectiveO1.serre_vanishingline 31