OAI/Algebra/Determinantal/SmoothSlices.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PermanentBorder.SliceParameters.homogeneous_aeval_scale line 9
  2. lemma OAI.PermanentBorder.CI.normalized_eval_zero_iff line 30
  3. lemma OAI.PermanentBorder.CI.good_derivative_invertible line 43
  4. lemma OAI.PermanentBorder.CI.fderiv_parameter_slice line 60
  5. def OAI.PermanentBorder.CI.linearEval line 69
  6. lemma OAI.PermanentBorder.CI.linearEval_apply line 74
  7. abbrev OAI.PermanentBorder.CI.FamilyRoots line 78
  8. def OAI.PermanentBorder.CI.familyProjection line 83
  9. lemma OAI.PermanentBorder.CI.normalized_family_proper line 86
  10. lemma OAI.PermanentBorder.CI.normalized_family_local line 117
  11. def OAI.PermanentBorder.CI.familyFiberEquiv line 145
  12. theorem OAI.PermanentBorder.CI.normalized_count_constant line 158
  13. lemma OAI.PermanentBorder.SliceParameters.variable_power_certificate line 184
  14. lemma OAI.PermanentBorder.SliceParameters.monomial_mem_of_variable_powers line 195
  15. theorem OAI.PermanentBorder.SliceParameters.homogeneous_piece_certificate line 213
  16. abbrev OAI.PermanentBorder.SliceParameters.DegreeIndex line 235
  17. instance OAI.PermanentBorder.SliceParameters.degreeIndex_finite line 237
  18. instance OAI.PermanentBorder.SliceParameters.degreeIndex_fintype line 245
  19. lemma OAI.PermanentBorder.SliceParameters.intWeight_degree line 248
  20. lemma OAI.PermanentBorder.SliceParameters.homogeneous_intWeight line 252
  21. lemma OAI.PermanentBorder.SliceParameters.intWeight_homogeneous line 262
  22. lemma OAI.PermanentBorder.SliceParameters.homogeneous_sum_degree line 271
  23. lemma OAI.PermanentBorder.SliceParameters.coeff_sum_degree line 295
  24. lemma OAI.PermanentBorder.SliceParameters.sum_degree_homogeneous line 306
  25. lemma OAI.PermanentBorder.SliceParameters.homogeneous_ext_degree line 314
  26. def OAI.PermanentBorder.SliceParameters.macaulayMatrix line 330
  27. def OAI.PermanentBorder.SliceParameters.macaulayCombination line 334
  28. lemma OAI.PermanentBorder.SliceParameters.coeff_macaulayCombination line 338
  29. lemma OAI.PermanentBorder.SliceParameters.macaulayCombination_mem line 345
  30. lemma OAI.PermanentBorder.SliceParameters.macaulayCombination_homogeneous line 353
  31. lemma OAI.PermanentBorder.SliceParameters.macaulayMatrix_map line 367
  32. theorem OAI.PermanentBorder.SliceParameters.macaulay_surjective_iff line 381