OAI/Algebra/Determinantal/PointBounds.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PermanentBorder.Multigraded.affine_cokernel_polynomial line 10
  2. theorem OAI.PermanentBorder.Multigraded.generic_homogeneous_quotient_bound line 45
  3. theorem OAI.PermanentBorder.Multigraded.generic_product_piece_bound line 69
  4. lemma OAI.PermanentBorder.Multigraded.normalized_pair_separator line 109
  5. lemma OAI.PermanentBorder.Multigraded.normalized_padding_homogeneous line 128
  6. lemma OAI.PermanentBorder.Multigraded.normalized_padding_eval line 142
  7. theorem OAI.PermanentBorder.Multigraded.normalized_interpolation line 150
  8. theorem OAI.PermanentBorder.Multigraded.normalized_points_le_pieceDim line 204
  9. def OAI.PermanentBorder.PolarAnalysis.SimpleAt line 252
  10. theorem OAI.PermanentBorder.PolarAnalysis.isInvertible_iff_isUnit line 255
  11. theorem OAI.PermanentBorder.PolarAnalysis.isOpen_simple line 265
  12. theorem OAI.PermanentBorder.PolarAnalysis.simple_branch line 273
  13. theorem OAI.PermanentBorder.PolarAnalysis.finite_simple_zeros_persist line 287
  14. theorem OAI.PermanentBorder.PolarAnalysis.fderiv_slice line 317
  15. theorem OAI.PermanentBorder.PolarAnalysis.contDiff_mvPolynomial_eval line 332
  16. theorem OAI.PermanentBorder.Multigraded.product_simple_point_bound_chart line 348