OAI/Combinatorics/SumProduct/Alignment/BooleanBinomial01.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HorizontalCubeCharacter.faceLift line 29
  2. lemma OAI.HorizontalCubeCharacter.faceLift_coe line 36
  3. lemma OAI.HorizontalCubeCharacter.eq_one_of_faces line 41
  4. lemma OAI.HorizontalCubeCharacter.split_face line 58
  5. structure OAI.HorizontalCubeCharacter.MaximalFace line 68
  6. theorem OAI.HorizontalCubeCharacter.exists_maximalFace line 83
  7. structure OAI.HorizontalCubeCharacter.LevelCharacter line 131
  8. def OAI.HorizontalCubeCharacter.MaximalFace.character line 142
  9. lemma OAI.HorizontalCubeCharacter.MaximalFace.character_nontrivial line 164
  10. abbrev OAI.BooleanBinomial.Exponent line 186
  11. def OAI.BooleanBinomial.degree line 188
  12. def OAI.BooleanBinomial.incrementSupport line 190
  13. lemma OAI.BooleanBinomial.mem_incrementSupport line 194
  14. def OAI.BooleanBinomial.part line 197
  15. lemma OAI.BooleanBinomial.coeff_part line 201
  16. lemma OAI.BooleanBinomial.part_support line 205
  17. lemma OAI.BooleanBinomial.sum_parts line 211
  18. def OAI.BooleanBinomial.composeSum line 217
  19. lemma OAI.BooleanBinomial.coeff_composeSum line 220
  20. def OAI.BooleanBinomial.binomial line 238
  21. lemma OAI.BooleanBinomial.binomial_eval line 241
  22. lemma OAI.BooleanBinomial.binomial_coeff_top line 246
  23. lemma OAI.BooleanBinomial.binomial_coeff_above line 252
  24. def OAI.BooleanBinomial.cubeBinomial line 257
  25. def OAI.BooleanBinomial.faceBinomial line 259
  26. lemma OAI.BooleanBinomial.faceBinomial_coeff line 262
  27. lemma OAI.BooleanBinomial.faceBinomial_support line 267
  28. def OAI.BooleanBinomial.isolatedExponent line 278
  29. lemma OAI.BooleanBinomial.isolatedExponent_none line 283
  30. lemma OAI.BooleanBinomial.isolatedExponent_some line 286
  31. lemma OAI.BooleanBinomial.isolatedExponent_support line 290
  32. lemma OAI.BooleanBinomial.degree_eq_sum line 296
  33. lemma OAI.BooleanBinomial.isolatedExponent_degree line 300
  34. lemma OAI.BooleanBinomial.isolatedExponent_multinomial line 306
  35. theorem OAI.BooleanBinomial.isolated_coefficient line 319
  36. lemma OAI.BooleanBinomial.coefficient_other_face line 331
  37. lemma OAI.BooleanBinomial.coefficient_lower_order line 335
  38. theorem OAI.BooleanBinomial.horizontal_coefficient line 343
  39. def OAI.BooleanBinomial.mask line 361
  40. lemma OAI.BooleanBinomial.masked_monomial line 365
  41. lemma OAI.BooleanBinomial.part_mask_eval line 384
  42. lemma OAI.BooleanBinomial.eval_composeSum line 400
  43. lemma OAI.BooleanBinomial.cubeBinomial_eval line 405
  44. theorem OAI.BooleanBinomial.binomial_expansion line 410
  45. lemma OAI.BooleanBinomial.boolean_product line 426
  46. theorem OAI.BooleanBinomial.boolean_binomial_expansion line 438
  47. lemma OAI.BooleanBinomial.incrementSupport_card_le line 449
  48. theorem OAI.BooleanBinomial.faceBinomial_vanish line 461