OAI/AlgebraicGeometry/Seshadri/Jets/AnalyticNode.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MaximalSeshadri.AnalyticNode.analytic_square_root line 17
2. lemma OAI.MaximalSeshadri.AnalyticNode.exists_nonzero_shear line 41
3. def OAI.MaximalSeshadri.AnalyticNode.nodeLinear line 58
4. lemma OAI.MaximalSeshadri.AnalyticNode.nodeLinear_apply line 64
5. lemma OAI.MaximalSeshadri.AnalyticNode.nodeLinear_bijective line 67
6. theorem OAI.MaximalSeshadri.AnalyticNode.analytic_node_inverse line 84
7. def OAI.MaximalSeshadri.AnalyticNode.shearLinear line 164
8. lemma OAI.MaximalSeshadri.AnalyticNode.shearLinear_apply line 168
9. lemma OAI.MaximalSeshadri.AnalyticNode.shearLinear_bijective line 171
10. theorem OAI.MaximalSeshadri.AnalyticNode.analytic_node_normal_form line 182