OAI/Algebra/Determinantal/Model.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PermanentBorder.Polar.isInvertible_of_injective line 9
  2. lemma OAI.PermanentBorder.Polar.normalizer_simple_restrict line 15
  3. theorem OAI.PermanentBorder.Polar.smooth_polar_affine_certificate line 59
  4. abbrev OAI.PermanentBorder.Variables line 120

    Also declared: ComparatorChallenges/PermanentCubic.lean:10 (same declaration text).

  5. abbrev OAI.PermanentBorder.Poly line 121

    Also declared: ComparatorChallenges/PermanentCubic.lean:11 (same declaration text), ComparatorChallenges/SmoothInitialForm.lean:11 (same declaration text).

  6. def OAI.PermanentBorder.permanentPolynomial line 123

    Also declared: ComparatorChallenges/PermanentCubic.lean:13 (same declaration text).

  7. def OAI.PermanentBorder.affineMatrixPolynomial line 126

    Also declared: ComparatorChallenges/PermanentCubic.lean:16 (same declaration text), ComparatorChallenges/SmoothInitialForm.lean:13 (same declaration text).

  8. def OAI.PermanentBorder.HasBorderDeterminant line 132

    Also declared: ComparatorChallenges/PermanentCubic.lean:22 (same declaration text), ComparatorChallenges/SmoothInitialForm.lean:19 (same declaration text).

  9. def OAI.PermanentBorder.HasExactDeterminant line 139

    Also declared: ComparatorChallenges/PermanentCubic.lean:29 (same declaration text), ComparatorChallenges/SmoothInitialForm.lean:26 (same declaration text).

  10. theorem OAI.PermanentBorder.HasExactDeterminant.hasBorderDeterminant line 143
  11. def OAI.PermanentBorder.exponentCube line 161
  12. theorem OAI.PermanentBorder.mem_exponentCube line 166
  13. theorem OAI.PermanentBorder.support_subset_exponentCube line 172
  14. theorem OAI.PermanentBorder.sum_over_exponentCube line 179
  15. theorem OAI.PermanentBorder.coeff_linear_map_cube line 189
  16. theorem OAI.PermanentBorder.support_subset_cube_of_limit line 200
  17. theorem OAI.PermanentBorder.coefficientwise_linear_map_limit line 216
  18. theorem OAI.PermanentBorder.degree_affine_form line 235
  19. theorem OAI.PermanentBorder.degree_affineMatrixPolynomial line 244
  20. def OAI.PermanentBorder.affineSubstitution line 264

    Distinct definitions of this name: ComparatorChallenges/SmoothInitialForm.lean:30 (different declaration text). Qualify references as OAI.PermanentBorder.affineSubstitution@path.

  21. theorem OAI.PermanentBorder.affineSubstitution_matrix line 268
  22. theorem OAI.PermanentBorder.HasBorderDeterminant.affineSubstitution line 292
  23. theorem OAI.PermanentBorder.affineMatrixPolynomial_scaleRow line 314
  24. theorem OAI.PermanentBorder.HasBorderDeterminant.smul line 344
  25. theorem OAI.PermanentBorder.HasBorderDeterminant.affineSubstitution_smul line 355