OAI/Combinatorics/Chromatic/GradedAlgebra/PowerSeriesSplitLeading.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.PowerSeriesSplit.pair_congr line 13
  2. lemma OAI.ElementaryPositivity.PowerSeriesSplit.left_coeff_congr line 28
  3. lemma OAI.ElementaryPositivity.PowerSeriesSplit.right_coeff_congr line 31
  4. lemma OAI.ElementaryPositivity.PowerSeriesSplit.leading_difference line 35
  5. lemma OAI.ElementaryPositivity.PowerSeriesSplit.zero_leading_difference line 51
  6. lemma OAI.ElementaryPositivity.PowerSeriesSplit.zero_coeff_congr line 62
  7. lemma OAI.ElementaryPositivity.FormalLog.mul_coeff_congr line 76
  8. lemma OAI.ElementaryPositivity.FormalLog.pow_coeff_congr line 85
  9. lemma OAI.ElementaryPositivity.FormalLog.pow_coeff_congr_of_two_le line 96
  10. def OAI.ElementaryPositivity.FormalLog.log line 115
  11. lemma OAI.ElementaryPositivity.FormalLog.log_constant line 118
  12. lemma OAI.ElementaryPositivity.FormalLog.log_coeff_congr line 122
  13. lemma OAI.ElementaryPositivity.FormalLog.log_coeff_succ line 132
  14. lemma OAI.ElementaryPositivity.FormalLog.log_leading_difference line 141