OAI/Algebra/Determinantal/HomogeneousPadding.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PermanentBorder.Selector.weight_one_sumElim line 8
  2. theorem OAI.PermanentBorder.Selector.homogeneous_coefficient line 14
  3. def OAI.PermanentBorder.Selector.universalHomogeneousPencil line 25
  4. theorem OAI.PermanentBorder.Selector.universalHomogeneousPencil_permanent line 30
  5. theorem OAI.PermanentBorder.Selector.coefficientPolynomial_homogeneous line 44
  6. def OAI.PermanentBorder.HomogeneousPadding.dehomogenize line 71
  7. theorem OAI.PermanentBorder.HomogeneousPadding.weight_optionElim line 74
  8. theorem OAI.PermanentBorder.HomogeneousPadding.weight_some line 80
  9. theorem OAI.PermanentBorder.HomogeneousPadding.dehomogenize_coeff_of_homogeneous line 85
  10. theorem OAI.PermanentBorder.HomogeneousPadding.homogeneous_eq_of_dehomogenize_eq line 104
  11. theorem OAI.PermanentBorder.HomogeneousPadding.dehomogenize_C line 118
  12. theorem OAI.PermanentBorder.HomogeneousPadding.dehomogenize_none line 121
  13. theorem OAI.PermanentBorder.HomogeneousPadding.dehomogenize_some line 124
  14. theorem OAI.PermanentBorder.HomogeneousPadding.dehomogenize_rename line 127
  15. def OAI.PermanentBorder.HomogeneousPadding.affineSubstitution line 135
  16. def OAI.PermanentBorder.HomogeneousPadding.homogeneousSubstitution line 138
  17. theorem OAI.PermanentBorder.HomogeneousPadding.dehomogenize_homogeneousSubstitution line 143
  18. theorem OAI.PermanentBorder.HomogeneousPadding.independent_padding line 160
  19. theorem OAI.PermanentBorder.permanentPolynomial_homogeneous line 177
  20. theorem OAI.PermanentBorder.coefficientPolynomial_homogeneous line 187
  21. theorem OAI.PermanentBorder.exists_selector_projection_homogeneous line 192
  22. lemma OAI.PermanentBorder.Selector.diagonalCoefficient_map line 219
  23. def OAI.PermanentBorder.Selector.integralCoefficientFamily line 237
  24. lemma OAI.PermanentBorder.Selector.integralCoefficientFamily_homogeneous line 241
  25. lemma OAI.PermanentBorder.Selector.integralCoefficientFamily_specialize line 246
  26. lemma OAI.PermanentBorder.Selector.integralCoefficientFamily_complex line 256
  27. theorem OAI.PermanentBorder.AlgebraicDimension.krullDim_le_of_injective_integral line 266
  28. theorem OAI.PermanentBorder.AlgebraicDimension.trdeg_le_of_krullDim_le line 288
  29. theorem OAI.PermanentBorder.AlgebraicDimension.field_image_trdeg_le line 306
  30. theorem OAI.PermanentBorder.AlgebraicDimension.point_field_trdeg_le line 318
  31. lemma OAI.PermanentBorder.SliceParameters.field_adjoin_trdeg_le line 349
  32. lemma OAI.PermanentBorder.SliceParameters.add_parameters line 372
  33. lemma OAI.PermanentBorder.SliceParameters.independent_card_le line 390