OAI/Algebra/Determinantal/ConditionalBound.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PermanentBorder.SliceParameters.singularSystem_map line 8
  2. def OAI.PermanentBorder.SliceParameters.universalSection line 15
  3. lemma OAI.PermanentBorder.SliceParameters.universalSection_specialize line 20
  4. lemma OAI.PermanentBorder.SliceParameters.universalSection_macaulay_map line 35
  5. theorem OAI.PermanentBorder.SliceParameters.transfer_section_certificate line 48
  6. lemma OAI.PermanentBorder.SliceParameters.macaulay_no_nonzero_zero line 81
  7. theorem OAI.PermanentBorder.SliceParameters.certificate_smooth_equations line 99
  8. abbrev OAI.PermanentBorder.SliceParameters.GenericClosed line 118
  9. def OAI.PermanentBorder.SliceParameters.independentParameters line 120
  10. lemma OAI.PermanentBorder.SliceParameters.independentParameters_independent line 124
  11. lemma OAI.PermanentBorder.SliceParameters.specialize_tower line 139
  12. theorem OAI.PermanentBorder.SliceParameters.exists_complex_smooth_section line 147
  13. lemma OAI.PermanentBorder.SliceParameters.gradientIdeal_rename line 184
  14. lemma OAI.PermanentBorder.SliceParameters.gradientDimension_rename line 200
  15. lemma OAI.PermanentBorder.SliceParameters.nonzero_of_gradientDimension line 207
  16. theorem OAI.PermanentBorder.SliceParameters.exists_complex_smooth_section_finite line 225
  17. abbrev OAI.PermanentBorder.Parameters.auxiliarySize line 270
  18. abbrev OAI.PermanentBorder.Parameters.selectorIndex line 271
  19. abbrev OAI.PermanentBorder.Parameters.selectorDegree line 272
  20. abbrev OAI.PermanentBorder.Parameters.defectThreshold line 273
  21. abbrev OAI.PermanentBorder.Parameters.codimension line 274
  22. abbrev OAI.PermanentBorder.Parameters.sectionDimension line 275
  23. theorem OAI.PermanentBorder.Parameters.size_bound line 277
  24. theorem OAI.PermanentBorder.Parameters.index_bounds line 286
  25. theorem OAI.PermanentBorder.Parameters.defect_formula line 300
  26. theorem OAI.PermanentBorder.Parameters.codimension_bounds line 306
  27. theorem OAI.PermanentBorder.Parameters.section_bounds line 335
  28. theorem OAI.PermanentBorder.Parameters.explicit_constant line 359
  29. lemma OAI.PermanentBorder.SliceParameters.linearSection_eq_affineSubstitution line 386
  30. theorem OAI.PermanentBorder.HasBorderDeterminant.selector_lower_of_critical_dimension line 393