OAI/Algebra/Determinantal/RankTransfer.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PermanentBorder.SliceParameters.exists_matrix_right_inverse line 8
2. theorem OAI.PermanentBorder.SliceParameters.integer_polynomial_rank_transfer line 19
3. theorem OAI.PermanentBorder.SliceParameters.polynomial_rank_specialize line 82
4. lemma OAI.PermanentBorder.Polar.smooth_extension line 141
5. lemma OAI.PermanentBorder.Polar.generic_bad_zero line 173
6. def OAI.PermanentBorder.Polar.universalBadPolar line 199
7. lemma OAI.PermanentBorder.Polar.universalBadPolar_specialize line 204
8. theorem OAI.PermanentBorder.Polar.exists_good_polar_certificate line 214
9. def OAI.PermanentBorder.Polar.hypersurfacePolars line 265
10. def OAI.PermanentBorder.Polar.hypersurfaceDegrees line 269
11. lemma OAI.PermanentBorder.Polar.hypersurfacePolars_homogeneous line 271
12. def OAI.PermanentBorder.Polar.swapFirstRows line 278
13. lemma OAI.PermanentBorder.Polar.hypersurfacePolars_square line 284
14. lemma OAI.PermanentBorder.Polar.determinant_permutation_ne_zero line 292
15. lemma OAI.PermanentBorder.Polar.polar_certificate_good line 301
16. theorem OAI.PermanentBorder.Polar.smooth_polar_count line 323
17. def OAI.PermanentBorder.Polar.coordinateSplit line 344
18. lemma OAI.PermanentBorder.Polar.coordinateSplit_none line 377
19. lemma OAI.PermanentBorder.Polar.exists_normalizer_equiv line 380
20. def OAI.PermanentBorder.Polar.optionInsert line 401
21. lemma OAI.PermanentBorder.Polar.optionInsert_none line 407
22. lemma OAI.PermanentBorder.Polar.optionInsert_some line 409
23. def OAI.PermanentBorder.Polar.affineNormChart line 411
24. lemma OAI.PermanentBorder.Polar.affineNormChart_hasFDerivAt line 415
25. lemma OAI.PermanentBorder.Polar.affineNormChart_contDiff line 426
26. lemma OAI.PermanentBorder.Polar.affineNormChart_injective line 436
27. lemma OAI.PermanentBorder.Polar.exists_chart_preimage line 443
28. lemma OAI.PermanentBorder.Polar.affineNormChart_eq line 452