OAI/Probability/SignedSweeps/CoefficientPush.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SignedSweeps.coefficientPush line 11
  2. lemma OAI.SignedSweeps.coefficientPush_apply line 15
  3. lemma OAI.SignedSweeps.coefficientPush_zero line 20
  4. lemma OAI.SignedSweeps.coefficientAction_injective line 26
  5. lemma OAI.SignedSweeps.coefficientAction_push line 44
  6. lemma OAI.SignedSweeps.coefficientPush_product line 53
  7. lemma OAI.SignedSweeps.coefficientPush_one line 59
  8. lemma OAI.SignedSweeps.coefficientPush_star line 65
  9. lemma OAI.SignedSweeps.coefficientPush_support line 73
  10. def OAI.SignedSweeps.productCoefficient line 87
  11. lemma OAI.SignedSweeps.productCoefficient_product line 89
  12. lemma OAI.SignedSweeps.productCoefficient_star line 97
  13. lemma OAI.SignedSweeps.productCoefficient_one line 103
  14. def OAI.SignedSweeps.coefficientPower line 125
  15. def OAI.SignedSweeps.coefficientListProduct line 129
  16. lemma OAI.SignedSweeps.coefficientAction_power line 143
  17. lemma OAI.SignedSweeps.coefficientAction_listProduct line 150
  18. lemma OAI.SignedSweeps.coefficientPush_power line 156
  19. lemma OAI.SignedSweeps.productCoefficient_power line 162