OAI/NumberTheory/PiExponent/Geometry/ProjectiveSpaceBasics.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.PiExponent.ProjectiveO1.projectiveSpace_noetherian line 12
2. instance OAI.PiExponent.ProjectiveO1.projectiveSpace_separated line 20
3. instance OAI.PiExponent.ProjectiveO1.projectiveSpace_diagonal_affine line 26
4. theorem OAI.PiExponent.ProjectiveO1.scalars_eq_baseScalars line 30