OAI/Algebra/OddKaplansky/Augmentation.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.OddKaplansky.Augmentation.C line 15
  2. abbrev OAI.OddKaplansky.Augmentation.R line 16
  3. def OAI.OddKaplansky.Augmentation.coordinate line 18
  4. def OAI.OddKaplansky.Augmentation.delta line 19
  5. def OAI.OddKaplansky.Augmentation.X line 20
  6. lemma OAI.OddKaplansky.Augmentation.coordinate_pow line 22
  7. instance OAI.OddKaplansky.Augmentation.(instance at line 32) line 32
  8. lemma OAI.OddKaplansky.Augmentation.X_pow line 35
  9. lemma OAI.OddKaplansky.Augmentation.delta_product line 42
  10. def OAI.OddKaplansky.Augmentation.shiftPolynomial line 68
  11. def OAI.OddKaplansky.Augmentation.eval line 70
  12. lemma OAI.OddKaplansky.Augmentation.eval_shiftPolynomial line 72
  13. lemma OAI.OddKaplansky.Augmentation.degreeOf_shiftPolynomial line 77
  14. def OAI.OddKaplansky.Augmentation.monomial line 103
  15. def OAI.OddKaplansky.Augmentation.monomialSpan line 105
  16. lemma OAI.OddKaplansky.Augmentation.eval_mem_span line 107
  17. lemma OAI.OddKaplansky.Augmentation.span_eq_top line 132
  18. lemma OAI.OddKaplansky.Augmentation.monomial_independent line 155
  19. def OAI.OddKaplansky.Augmentation.gridBasis line 161
  20. lemma OAI.OddKaplansky.Augmentation.gridBasis_apply line 163
  21. lemma OAI.OddKaplansky.Augmentation.eval_zero_of_high_degree line 166
  22. lemma OAI.OddKaplansky.Augmentation.eval_ideal_power line 189
  23. def OAI.OddKaplansky.Augmentation.exponents line 204
  24. lemma OAI.OddKaplansky.Augmentation.exponents_apply line 205
  25. lemma OAI.OddKaplansky.Augmentation.degree_exponents line 211
  26. lemma OAI.OddKaplansky.Augmentation.eval_monomial line 220
  27. lemma OAI.OddKaplansky.Augmentation.shiftPolynomial_sub_one_mem line 236
  28. lemma OAI.OddKaplansky.Augmentation.annihilates_monomial line 257