OAI/Combinatorics/Progressions/Linear/BasisGradedCoordinateBasis.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.supportedSubmoduleBasis line 19
  2. theorem OAI.Erdos3.supportedSubmoduleBasis_coe line 29
  3. theorem OAI.Erdos3.supportedSubmoduleBasis_repr line 34
  4. theorem OAI.Erdos3.basis_mem_span_image_iff line 47
  5. def OAI.Erdos3.basisCoordinateProjection line 71
  6. theorem OAI.Erdos3.basisCoordinateProjection_repr line 78
  7. theorem OAI.Erdos3.basisCoordinateProjection_mem_span line 85
  8. theorem OAI.Erdos3.basisCoordinateProjection_eq_self line 92
  9. theorem OAI.Erdos3.basisCoordinateProjection_basis line 102
  10. theorem OAI.Erdos3.basisCoordinateProjection_idempotent line 114
  11. theorem OAI.Erdos3.basisCoordinateProjection_eq_zero_iff line 118
  12. theorem OAI.Erdos3.sub_basisCoordinateProjection_mem line 135
  13. theorem OAI.Erdos3.basisCoordinateProjection_eq_iff line 140
  14. theorem OAI.Erdos3.basis_isCompl_span_compl line 157
  15. def OAI.Erdos3.supportedQuotientBasis line 163
  16. theorem OAI.Erdos3.supportedQuotientBasis_apply line 169
  17. theorem OAI.Erdos3.supportedQuotientBasis_repr_mk line 175
  18. theorem OAI.Erdos3.supportedQuotientBasis_map_span line 194
  19. def OAI.Erdos3.basisGradeProjection line 231
  20. def OAI.Erdos3.basisBelowProjection line 234
  21. theorem OAI.Erdos3.basisGradeProjection_repr line 237
  22. theorem OAI.Erdos3.basisBelowProjection_repr line 241
  23. theorem OAI.Erdos3.basisBelowProjection_eq_sum_grades line 245
  24. def OAI.Erdos3.BasisGradedSubmodule line 251
  25. theorem OAI.Erdos3.BasisGradedSubmodule.below_mem line 254
  26. theorem OAI.Erdos3.sub_basisBelowProjection_mem line 260
  27. theorem OAI.Erdos3.basisBelowProjection_eq_iff line 265
  28. theorem OAI.Erdos3.BasisGradedSubmodule.below_mem_of_mem_sup line 271
  29. theorem OAI.Erdos3.basisGradeProjection_pi_apply line 295
  30. theorem OAI.Erdos3.sum_basisGradeProjection_pi line 302
  31. theorem OAI.Erdos3.basisGraded_homogeneous_span line 309
  32. theorem OAI.Erdos3.exists_basisGraded_coordinate_basis line 330
  33. theorem OAI.Erdos3.exists_basisGraded_coordinate_basis_bounded line 350