OAI/Combinatorics/SumProduct/Alignment/RationalLattice14.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RationalLattice.log_multiplication_weighted line 27
  2. theorem OAI.RationalLattice.log_left_displacement_weighted line 48
  3. lemma OAI.RationalLattice.canonicalLog_congr_prefix line 88
  4. lemma OAI.RationalLattice.canonicalLog_mul_prefix line 97
  5. lemma OAI.RationalLattice.mem_level_iff_log line 108
  6. lemma OAI.RationalLattice.canonicalExp_mem_level_iff line 117
  7. lemma OAI.RationalLattice.canonicalLog_mul_level line 123
  8. theorem OAI.RationalLattice.logHomLinear_lowers_of_displacement line 133
  9. lemma OAI.WeightedPolynomial.IsWeighted.smul line 160
  10. lemma OAI.WeightedPolynomial.IsWeighted.sum line 165
  11. lemma OAI.WeightedPolynomial.IsWeighted.linear line 175
  12. lemma OAI.WeightedPolynomial.eval_kill_inl line 213
  13. lemma OAI.WeightedPolynomial.exists_right_of_vanishing line 226
  14. lemma OAI.WeightedPolynomial.weight_lt_of_other line 247
  15. lemma OAI.WeightedPolynomial.mixed_weight_strict line 262
  16. theorem OAI.WeightedPolynomial.mixed_eval_congr line 283