OAI/Algebra/Determinantal/SingularValues.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PermanentBorder.CurveFamily.add_evaluated_polynomial line 10
2. lemma OAI.PermanentBorder.CurveFamily.evaluated_mem line 42
3. lemma OAI.PermanentBorder.CurveFamily.add_algebraic_closure line 46
4. lemma OAI.PermanentBorder.CurveFamily.node_values_mem line 59
5. theorem OAI.PermanentBorder.CurveFamily.adjoin_polynomial_family line 97
6. def OAI.PermanentBorder.CurveFamily.pointEvaluation line 118
7. lemma OAI.PermanentBorder.CurveFamily.pointEvaluation_apply line 121
8. theorem OAI.PermanentBorder.CurveFamily.node_parameter_bound line 125
9. abbrev OAI.PermanentBorder.FrobeniusPlane.Plane line 171
10. def OAI.PermanentBorder.FrobeniusPlane.squareForm line 173
11. lemma OAI.PermanentBorder.FrobeniusPlane.squareForm_add line 176
12. lemma OAI.PermanentBorder.FrobeniusPlane.squareForm_mul_zero line 184
13. lemma OAI.PermanentBorder.FrobeniusPlane.squareForm_mul_one line 190
14. theorem OAI.PermanentBorder.FrobeniusPlane.exists_squareForm line 195
15. lemma OAI.PermanentBorder.FrobeniusPlane.pderiv_square line 212
16. lemma OAI.PermanentBorder.FrobeniusPlane.squareForm_partial_zero line 216
17. lemma OAI.PermanentBorder.FrobeniusPlane.squareForm_partial_one line 221
18. lemma OAI.PermanentBorder.FrobeniusPlane.squareForm_mixed line 226
19. theorem OAI.PermanentBorder.FrobeniusPlane.wild_zero_iff line 232
20. lemma OAI.PermanentBorder.FrobeniusPlane.squareForm_eq_zero_iff line 259
21. lemma OAI.PermanentBorder.FrobeniusPlane.squareForm_injective line 280
22. lemma OAI.PermanentBorder.FrobeniusPlane.wild_ideal_eq line 290
23. lemma OAI.PermanentBorder.FrobeniusPlane.squareForm_mul line 338
24. theorem OAI.PermanentBorder.FrobeniusPlane.existsUnique_squareForm line 343