OAI/Analysis/SymmetricDomains/FiberPolynomialNatDegree.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Release061.exists_algHom_separating_element line 16
2. theorem OAI.Release061.normalization_proper_finite line 36
3. theorem OAI.Release061.finite_algebra_complex_points_isOpenMap line 85
4. theorem OAI.Release061.normalization_isOpenMap line 129
5. theorem OAI.Release061.normalization_analytic_sheets line 153
6. def OAI.Release061.fiberPolynomial line 211
7. theorem OAI.Release061.fiberPolynomial_eq_prod line 216
8. theorem OAI.Release061.fiberPolynomial_eval_eq_zero line 235
9. theorem OAI.Release061.fiberPolynomial_monic line 244
10. theorem OAI.Release061.fiberPolynomial_natDegree line 250