OAI/Algebra/Determinantal/WildParameters.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PermanentBorder.CurveFamily.twice_choose_two line 10
2. lemma OAI.PermanentBorder.CurveFamily.even_count line 18
3. lemma OAI.PermanentBorder.CurveFamily.odd_count line 29
4. theorem OAI.PermanentBorder.CurveFamily.wild_parameter_bound_even line 38
5. theorem OAI.PermanentBorder.CurveFamily.wild_parameter_bound_odd line 73
6. lemma OAI.PermanentBorder.CurveFamily.pointEvaluation_surjective line 116
7. lemma OAI.PermanentBorder.CurveFamily.partial_leading line 147
8. theorem OAI.PermanentBorder.CurveFamily.distinct_critical_point_count line 156
9. lemma OAI.PermanentBorder.FrobeniusPlane.squareForm_map line 186
10. lemma OAI.PermanentBorder.FrobeniusPlane.high_coeff_of_top line 193
11. lemma OAI.PermanentBorder.FrobeniusPlane.high_coeff_zero line 205
12. theorem OAI.PermanentBorder.FrobeniusPlane.fixed_half_forms_even line 211
13. theorem OAI.PermanentBorder.FrobeniusPlane.fixed_half_forms_odd line 237
14. theorem OAI.PermanentBorder.IdealColength.quotient_product_length line 269
15. lemma OAI.PermanentBorder.FrobeniusPlane.square_mem_of_mem_span line 316
16. theorem OAI.PermanentBorder.FrobeniusPlane.frobenius_quotient_bound line 325
17. def OAI.PermanentBorder.CurveFamily.zeroEvaluation line 381
18. lemma OAI.PermanentBorder.CurveFamily.zeroEvaluation_surjective line 388
19. lemma OAI.PermanentBorder.CurveFamily.finite_zeroLocus line 395
20. lemma OAI.PermanentBorder.CurveFamily.zero_card_le_finrank line 407
21. lemma OAI.PermanentBorder.CurveFamily.radical_length_eq_zero_card line 415