OAI/Algebra/Determinantal/ConductorDimension.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PermanentBorder.CurveFamily.singularIdeal line 9
  2. lemma OAI.PermanentBorder.CurveFamily.singular_zero_iff line 13
  3. lemma OAI.PermanentBorder.CurveFamily.singular_add_square_eq line 21
  4. lemma OAI.PermanentBorder.CurveFamily.singular_wild_card_le line 29
  5. lemma OAI.PermanentBorder.CurveFamily.singular_point_card_le line 53
  6. theorem OAI.PermanentBorder.CurveFamily.singular_enlarged_length line 67
  7. def OAI.PermanentBorder.PlaneBivariate.toBivariate line 102
  8. def OAI.PermanentBorder.PlaneBivariate.fromBivariate line 105
  9. lemma OAI.PermanentBorder.PlaneBivariate.to_zero line 108
  10. lemma OAI.PermanentBorder.PlaneBivariate.to_one line 109
  11. lemma OAI.PermanentBorder.PlaneBivariate.to_C line 110
  12. lemma OAI.PermanentBorder.PlaneBivariate.from_X line 112
  13. lemma OAI.PermanentBorder.PlaneBivariate.from_C_X line 113
  14. lemma OAI.PermanentBorder.PlaneBivariate.from_C_C line 114
  15. lemma OAI.PermanentBorder.PlaneBivariate.from_to line 117
  16. lemma OAI.PermanentBorder.PlaneBivariate.to_from line 121
  17. def OAI.PermanentBorder.PlaneBivariate.equiv line 127
  18. lemma OAI.PermanentBorder.PlaneBivariate.equiv_apply line 130
  19. lemma OAI.PermanentBorder.PlaneBivariate.equiv_symm_apply line 131
  20. lemma OAI.PermanentBorder.PlaneBivariate.derivative_to line 133
  21. lemma OAI.PermanentBorder.PlaneBivariate.map_to line 142
  22. def OAI.PermanentBorder.PlaneScaling.scale line 158
  23. lemma OAI.PermanentBorder.PlaneScaling.scale_monomial line 161
  24. lemma OAI.PermanentBorder.PlaneScaling.coeff_scale line 172
  25. lemma OAI.PermanentBorder.PlaneScaling.degree_le_of_scale line 186
  26. theorem OAI.PermanentBorder.Conductor.normalization_length_le_ideal line 208
  27. theorem OAI.PermanentBorder.Conductor.normalization_length_le_enlarged line 243
  28. lemma OAI.PermanentBorder.Conductor.equiv_ring_apply line 268
  29. lemma OAI.PermanentBorder.Conductor.map_singularIdeal line 270
  30. lemma OAI.PermanentBorder.Conductor.map_enlargedIdeal line 279
  31. theorem OAI.PermanentBorder.Conductor.normalization_length_le_half line 290
  32. lemma OAI.PermanentBorder.CurveFamily.inField_squareForm line 325
  33. lemma OAI.PermanentBorder.CurveFamily.singular_finite line 339
  34. theorem OAI.PermanentBorder.CurveFamily.ordinary_parameter_bound line 356
  35. lemma OAI.PermanentBorder.CurveFamily.halfIdeal_finite line 401
  36. lemma OAI.PermanentBorder.CurveFamily.ordinary_even_count line 412
  37. lemma OAI.PermanentBorder.CurveFamily.ordinary_odd_count line 420
  38. theorem OAI.PermanentBorder.CurveFamily.half_curve_parameter_bound line 430