OAI/Algebra/Determinantal/HalfPolynomials.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PermanentBorder.LinearParameters.add_constrained_parameters line 11
2. def OAI.PermanentBorder.CurveFamily.InField line 68
3. lemma OAI.PermanentBorder.CurveFamily.inField_lift line 71
4. lemma OAI.PermanentBorder.CurveFamily.inField_of_high line 78
5. lemma OAI.PermanentBorder.CurveFamily.span_low line 86
6. lemma OAI.PermanentBorder.CurveFamily.repr_polynomial_mem line 114
7. theorem OAI.PermanentBorder.CurveFamily.add_vanishing_polynomial line 129
8. lemma OAI.PermanentBorder.CurveFamily.adjoin_polynomial line 169
9. lemma OAI.PermanentBorder.CurveFamily.monomial_plane line 178
10. theorem OAI.PermanentBorder.CurveFamily.extend_by_quotient line 183
11. lemma OAI.PermanentBorder.CurveFamily.filtered_rank_le line 218
12. lemma OAI.PermanentBorder.CurveFamily.inField_map line 223
13. lemma OAI.PermanentBorder.CurveFamily.inField_mono line 229
14. theorem OAI.PermanentBorder.CurveFamily.add_vanishing_family line 232
15. theorem OAI.PermanentBorder.CurveFamily.four_polynomial_bound line 256
16. lemma OAI.PermanentBorder.FrobeniusPlane.derivation_square line 295
17. lemma OAI.PermanentBorder.FrobeniusPlane.derivation_zero_of_field_generators line 302
18. theorem OAI.PermanentBorder.FrobeniusPlane.finite_of_square_coordinate_equations line 332
19. theorem OAI.PermanentBorder.FrobeniusPlane.node_coordinates_algebraic line 363