OAI/Analysis/ModularTheory/AlgebraicNormalForm.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Normal ordering of algebraic modular-core elements. The finite sums here are taken in the concrete regular representation.

  1. abbrev OAI.WeakPureInfiniteness.translation line 17
  2. lemma OAI.WeakPureInfiniteness.translation_add line 23
  3. lemma OAI.WeakPureInfiniteness.translation_zero line 30
  4. lemma OAI.WeakPureInfiniteness.translation_star line 35
  5. lemma OAI.WeakPureInfiniteness.translation_coefficient line 39
  6. def OAI.WeakPureInfiniteness.modularCoreMonomial line 51
  7. def OAI.WeakPureInfiniteness.normalSpan line 55
  8. lemma OAI.WeakPureInfiniteness.monomial_one line 58
  9. lemma OAI.WeakPureInfiniteness.monomial_mul line 62
  10. lemma OAI.WeakPureInfiniteness.monomial_star line 76
  11. lemma OAI.WeakPureInfiniteness.normalSpan_mul line 84
  12. lemma OAI.WeakPureInfiniteness.normalSpan_star line 104
  13. def OAI.WeakPureInfiniteness.normalAlgebra line 120
  14. theorem OAI.WeakPureInfiniteness.algebraicModularCore_normal_form line 132