OAI/Combinatorics/Progressions/Linear/QuotientProjectionCoordinates.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.BasisBlockInvariant line 14
  2. theorem OAI.Erdos3.sum_basisBlockProjection line 17
  3. def OAI.Erdos3.blockSpanningFamily line 28
  4. theorem OAI.Erdos3.blockSpanningFamily_repr line 31
  5. theorem OAI.Erdos3.blockSpanningFamily_span line 36
  6. theorem OAI.Erdos3.blockSpanningFamily_height line 56
  7. theorem OAI.Erdos3.basisBlockMap_commutes line 80
  8. theorem OAI.Erdos3.BasisBlockInvariant.map line 101
  9. theorem OAI.Erdos3.basisBlockInvariant_ker line 110
  10. theorem OAI.Erdos3.BasisBlockInvariant.inf line 118
  11. def OAI.Erdos3.matrixBlockPart line 137
  12. theorem OAI.Erdos3.matrixBlockPart_eq line 141
  13. theorem OAI.Erdos3.matrixBlockPart_off_block line 149
  14. theorem OAI.Erdos3.matrix_mul_blockPart line 154
  15. theorem OAI.Erdos3.matrix_blockPart_mul line 171
  16. theorem OAI.Erdos3.matrixBlockPart_image_section line 188
  17. theorem OAI.Erdos3.exists_bounded_block_image_section line 197
  18. theorem OAI.Erdos3.real_matrix_image_section line 224
  19. theorem OAI.Erdos3.exists_real_span_defining_matrix line 232
  20. theorem OAI.Erdos3.real_column_span_mem_iff line 266
  21. theorem OAI.Erdos3.imageDefiningHeight_pos line 285
  22. theorem OAI.Erdos3.exists_bounded_block_quotient_projection line 292
  23. theorem OAI.Erdos3.exists_submodule_block_quotient_projection line 333
  24. theorem OAI.Erdos3.exists_real_block_span_defining_matrix line 369
  25. def OAI.Erdos3.quotientProjectionEquiv line 430
  26. theorem OAI.Erdos3.quotientProjectionEquiv_mk line 435
  27. theorem OAI.Erdos3.quotientProjectionEquiv_symm line 440