OAI/Algebra/Determinantal/SliceCertificates.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PermanentBorder.SliceParameters.homogeneous_piece_certificate_all line 8
  2. lemma OAI.PermanentBorder.SliceParameters.macaulay_surjective_zero line 25
  3. lemma OAI.PermanentBorder.CI.good_certificate_all line 50
  4. lemma OAI.PermanentBorder.CI.good_of_certificate line 66
  5. lemma OAI.PermanentBorder.CI.matrix_right_inverse line 79
  6. lemma OAI.PermanentBorder.CI.rank_curve line 89
  7. lemma OAI.PermanentBorder.CI.polynomial_nonzero_preconnected line 126
  8. lemma OAI.PermanentBorder.CI.map_linear line 139
  9. lemma OAI.PermanentBorder.CI.map_square line 144
  10. lemma OAI.PermanentBorder.CI.map_bad line 150
  11. def OAI.PermanentBorder.CI.Hline line 157
  12. def OAI.PermanentBorder.CI.lline line 160
  13. def OAI.PermanentBorder.CI.Htime line 162
  14. def OAI.PermanentBorder.CI.ltime line 164
  15. lemma OAI.PermanentBorder.CI.Htime_zero line 168
  16. lemma OAI.PermanentBorder.CI.Htime_one line 171
  17. lemma OAI.PermanentBorder.CI.ltime_zero line 174
  18. lemma OAI.PermanentBorder.CI.ltime_one line 177
  19. lemma OAI.PermanentBorder.CI.Hline_map line 181
  20. lemma OAI.PermanentBorder.CI.lline_eval line 187
  21. lemma OAI.PermanentBorder.CI.Htime_homogeneous line 191
  22. lemma OAI.PermanentBorder.CI.good_curve line 197
  23. lemma OAI.PermanentBorder.CI.linear_ltime line 234
  24. lemma OAI.PermanentBorder.CI.normalized_time line 240
  25. lemma OAI.PermanentBorder.CI.contDiff_normalized_time line 248
  26. theorem OAI.PermanentBorder.CI.good_card line 259
  27. def OAI.PermanentBorder.Polar.extendDerivation line 284
  28. lemma OAI.PermanentBorder.Polar.extendDerivation_algebraMap line 290
  29. abbrev OAI.PermanentBorder.Polar.GenericField line 300
  30. def OAI.PermanentBorder.Polar.genericParameter line 302
  31. lemma OAI.PermanentBorder.Polar.generic_formallyEtale line 305
  32. def OAI.PermanentBorder.Polar.parameterDerivation line 315
  33. lemma OAI.PermanentBorder.Polar.parameterDerivation_parameter line 321
  34. lemma OAI.PermanentBorder.Polar.derivation_aeval line 332