OAI/Algebra/Determinantal/Gradients.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PermanentBorder.GradientAlgebra.permanent_eq_det line 12
  2. theorem OAI.PermanentBorder.GradientAlgebra.derivation_prod line 25
  3. theorem OAI.PermanentBorder.GradientAlgebra.derivation_det_updateCol line 46
  4. theorem OAI.PermanentBorder.GradientAlgebra.derivation_det line 67
  5. def OAI.PermanentBorder.GradientAlgebra.coefficientPart line 80
  6. theorem OAI.PermanentBorder.GradientAlgebra.coeff_coefficientPart line 86
  7. theorem OAI.PermanentBorder.GradientAlgebra.coefficientPart_pderiv line 90
  8. def OAI.PermanentBorder.GradientAlgebra.genericPencil line 100
  9. theorem OAI.PermanentBorder.GradientAlgebra.pderiv_genericPencil line 106
  10. theorem OAI.PermanentBorder.GradientAlgebra.pderiv_det_genericPencil line 112
  11. theorem OAI.PermanentBorder.GradientAlgebra.coefficientPart_C_X_mul line 130
  12. theorem OAI.PermanentBorder.GradientAlgebra.coefficientPart_monomial line 137
  13. theorem OAI.PermanentBorder.GradientAlgebra.eval_coefficientPart line 145
  14. def OAI.PermanentBorder.GradientAlgebra.fixedPencil line 161
  15. theorem OAI.PermanentBorder.GradientAlgebra.eval_genericPencil line 165
  16. theorem OAI.PermanentBorder.GradientAlgebra.gradient_coefficient_identity line 171
  17. theorem OAI.PermanentBorder.GradientAlgebra.gradient_zero_iff_adjugate_coefficient line 185
  18. def OAI.PermanentBorder.GradientAlgebra.biCoefficientPart line 199
  19. theorem OAI.PermanentBorder.GradientAlgebra.coeff_biCoefficientPart line 207
  20. theorem OAI.PermanentBorder.GradientAlgebra.biCoefficientPart_pderiv line 211
  21. theorem OAI.PermanentBorder.GradientAlgebra.biCoefficientPart_monomial line 218
  22. theorem OAI.PermanentBorder.GradientAlgebra.eval_biCoefficientPart line 226
  23. def OAI.PermanentBorder.GradientAlgebra.genericAffinePencil line 241
  24. def OAI.PermanentBorder.GradientAlgebra.fixedAffinePencil line 246
  25. theorem OAI.PermanentBorder.GradientAlgebra.pderiv_genericAffinePencil line 252
  26. theorem OAI.PermanentBorder.GradientAlgebra.pderiv_det_genericAffinePencil line 257
  27. theorem OAI.PermanentBorder.GradientAlgebra.eval_genericAffinePencil line 271
  28. def OAI.PermanentBorder.GradientAlgebra.affineSelector line 277
  29. theorem OAI.PermanentBorder.GradientAlgebra.gradient_affineSelector line 280
  30. def OAI.PermanentBorder.Selector.bivariateToNested line 303
  31. lemma OAI.PermanentBorder.Selector.bivariateToNested_coeff line 307
  32. lemma OAI.PermanentBorder.Selector.bivariateToNested_C line 323
  33. lemma OAI.PermanentBorder.Selector.bivariateToNested_X_zero line 327
  34. lemma OAI.PermanentBorder.Selector.bivariateToNested_X_one line 333
  35. lemma OAI.PermanentBorder.Selector.commAlgEquiv_coeff_coeff line 342
  36. def OAI.PermanentBorder.Selector.interchangeBivariate line 359
  37. lemma OAI.PermanentBorder.Selector.biCoefficientPart_interchange line 364
  38. lemma OAI.PermanentBorder.Selector.interchangeBivariate_C_X line 371
  39. lemma OAI.PermanentBorder.Selector.interchangeBivariate_C_C line 375
  40. lemma OAI.PermanentBorder.Selector.interchangeBivariate_X_zero line 380
  41. lemma OAI.PermanentBorder.Selector.interchangeBivariate_X_one line 385
  42. lemma OAI.PermanentBorder.Selector.diagonalCoefficient_eq_affineSelector line 391