OAI/Analysis/FreeWords/LaurentSpan.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KKFreeWords.laurentAlgebra line 100
  2. def OAI.KKFreeWords.laurentSpan line 103
  3. def OAI.KKFreeWords.centeredLaurentSpan line 106
  4. theorem OAI.KKFreeWords.upow_mem_laurentSpan line 110
  5. theorem OAI.KKFreeWords.laurentSpan_mul line 114
  6. theorem OAI.KKFreeWords.laurentSpan_star line 132
  7. theorem OAI.KKFreeWords.laurentAlgebra_le_span line 144
  8. theorem OAI.KKFreeWords.centered_mem_laurentSpan line 158
  9. theorem OAI.KKFreeWords.trace_zero_laurent_mem_span line 180
  10. theorem OAI.KKFreeWords.linear_prod_zero_of_span line 188