OAI/NumberTheory/PiExponent/Geometry/ProjectiveTupleCharts.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.GeometrySupport.ProjectiveTupleCharts.tupleVariables line 16
2. theorem OAI.PiExponent.GeometrySupport.ProjectiveTupleCharts.mem_tupleVariables line 21
3. theorem OAI.PiExponent.GeometrySupport.ProjectiveTupleCharts.tupleVariables_support line 27
4. theorem OAI.PiExponent.GeometrySupport.ProjectiveTupleCharts.tupleVariables_support_subtuple line 41
5. theorem OAI.PiExponent.GeometrySupport.ProjectiveTupleCharts.tupleVariables_inf line 51
6. theorem OAI.PiExponent.GeometrySupport.ProjectiveTupleCharts.coordinateFiniteOpen_tuple line 69
7. abbrev OAI.PiExponent.GeometrySupport.ProjectiveTupleCharts.schemeFreeOpen line 82
8. def OAI.PiExponent.GeometrySupport.ProjectiveTupleCharts.freeOpenHomCongr line 85
9. theorem OAI.PiExponent.GeometrySupport.ProjectiveTupleCharts.freeOpenHomCongr_restrict line 99
10. theorem OAI.PiExponent.GeometrySupport.ProjectiveTupleCharts.coordinateOpen_isAffine line 120
11. def OAI.PiExponent.GeometrySupport.ProjectiveTupleCharts.coordinateTupleCoefficient line 126
12. theorem OAI.PiExponent.GeometrySupport.ProjectiveTupleCharts.coordinateTupleCoefficient_injective line 133
13. theorem OAI.PiExponent.GeometrySupport.ProjectiveTupleCharts.coordinateTupleCoefficient_regular line 138
14. theorem OAI.PiExponent.GeometrySupport.ProjectiveTupleCharts.coordinateTupleCoefficient_surjective_regular line 150