OAI/Analysis/SymmetricDomains/ChartDimensionLeCoordinate.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Release061.trdeg_ge_of_polynomial_local_retraction line 34
2. def OAI.Release061.linearCoordinatePolynomial line 70
3. theorem OAI.Release061.linearCoordinatePolynomial_eval line 74
4. theorem OAI.Release061.trdeg_ge_of_analytic_immersion line 88
5. theorem OAI.Release061.chart_dimension_le_coordinate_trdeg line 125