OAI/Combinatorics/Chromatic/GradedAlgebra/RootTruncation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RootTruncation.cut line 12
  2. lemma OAI.ElementaryPositivity.RootTruncation.coeff_cut line 14
  3. lemma OAI.ElementaryPositivity.RootTruncation.coeff_cut_of_le line 16
  4. lemma OAI.ElementaryPositivity.RootTruncation.constant_cut line 18
  5. lemma OAI.ElementaryPositivity.RootTruncation.cut_congr line 21
  6. lemma OAI.ElementaryPositivity.RootTruncation.cut_cut line 28
  7. lemma OAI.ElementaryPositivity.RootTruncation.cut_cut_le line 30
  8. lemma OAI.ElementaryPositivity.RootTruncation.cut_zeroFactor line 33
  9. lemma OAI.ElementaryPositivity.RootTruncation.cut_mul_cut line 39
  10. lemma OAI.ElementaryPositivity.RootTruncation.cut_list_product line 45
  11. def OAI.ElementaryPositivity.QuantumTorus.completedCut line 57
  12. lemma OAI.ElementaryPositivity.QuantumTorus.completedCut_supported line 65
  13. lemma OAI.ElementaryPositivity.QuantumTorus.completedCut_chartZero line 75
  14. lemma OAI.ElementaryPositivity.QuantumTorus.SeriesGraded.cut line 84
  15. lemma OAI.ElementaryPositivity.QuantumTorus.SeriesConverges.cut line 91