OAI/Combinatorics/Chromatic/GradedAlgebra/PowerSeriesSplit.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.PowerSeriesSplit.pairCoefficients line 12
  2. def OAI.ElementaryPositivity.PowerSeriesSplit.leftFactor line 21
  3. def OAI.ElementaryPositivity.PowerSeriesSplit.rightFactor line 23
  4. lemma OAI.ElementaryPositivity.PowerSeriesSplit.left_constant line 26
  5. lemma OAI.ElementaryPositivity.PowerSeriesSplit.right_constant line 30
  6. lemma OAI.ElementaryPositivity.PowerSeriesSplit.coeff_mul_succ line 35
  7. lemma OAI.ElementaryPositivity.PowerSeriesSplit.factorization line 46
  8. lemma OAI.ElementaryPositivity.PowerSeriesSplit.left_fixed line 58
  9. lemma OAI.ElementaryPositivity.PowerSeriesSplit.right_killed line 63
  10. lemma OAI.ElementaryPositivity.PowerSeriesSplit.uniqueness line 69
  11. lemma OAI.ElementaryPositivity.PowerSeriesSplit.factors_mem line 103
  12. lemma OAI.ElementaryPositivity.PowerSeriesSplit.mul_mem line 127
  13. lemma OAI.ElementaryPositivity.PowerSeriesSplit.factors_graded line 133