OAI/Combinatorics/Progressions/Linear/OrderedBasisCoordinates.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.mem_drop_finRange_iff line 14
  2. def OAI.Erdos3.orderedBasisTailProduct line 32
  3. def OAI.Erdos3.orderedBasisProduct line 36
  4. theorem OAI.Erdos3.orderedBasisTailProduct_terminal line 39
  5. theorem OAI.Erdos3.orderedBasisTailProduct_step line 45
  6. theorem OAI.Erdos3.orderedBasisTailProduct_congr line 52
  7. theorem OAI.Erdos3.IsCentralLieBasis.orderedBasisTailProduct_mem_tail line 65
  8. theorem OAI.Erdos3.IsCentralLieBasis.orderedBasisTailProduct_leading line 75
  9. theorem OAI.Erdos3.IsCentralLieBasis.exists_orderedBasisTailProduct_aux line 97
  10. theorem OAI.Erdos3.IsCentralLieBasis.exists_orderedBasisTailProduct line 138
  11. theorem OAI.Erdos3.IsCentralLieBasis.orderedBasisProduct_surjective line 143
  12. theorem OAI.Erdos3.IsCentralLieBasis.orderedBasisTailProduct_eq_of_product_eq line 147
  13. theorem OAI.Erdos3.IsCentralLieBasis.orderedBasisProduct_injective line 165
  14. def OAI.Erdos3.IsCentralLieBasis.orderedBasisEquiv line 172
  15. theorem OAI.Erdos3.IsCentralLieBasis.orderedBasisEquiv_apply line 176
  16. theorem OAI.Erdos3.IsCentralLieBasis.orderedBasisProduct_coordinates line 179