OAI/Computability/PerfectCompleteness/Algebra/BilinearGramCompressionLemmas.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.BilinearGramCompression.combinations line 30
  2. def OAI.PerfectCompleteness.BilinearGramCompression.crossGram line 33
  3. def OAI.PerfectCompleteness.BilinearGramCompression.gram line 37
  4. theorem OAI.PerfectCompleteness.BilinearGramCompression.crossGram_combinations line 41
  5. theorem OAI.PerfectCompleteness.BilinearGramCompression.gram_combinations line 57
  6. theorem OAI.PerfectCompleteness.BilinearGramCompression.cross_rank_le line 63
  7. theorem OAI.PerfectCompleteness.BilinearGramCompression.gram_rank_le line 71
  8. theorem OAI.PerfectCompleteness.BilinearGramCompression.cross_rank_le_one line 77
  9. def OAI.PerfectCompleteness.BilinearRestrictionRank.restrictForm line 100
  10. theorem OAI.PerfectCompleteness.BilinearRestrictionRank.restrictForm_apply line 105
  11. theorem OAI.PerfectCompleteness.BilinearRestrictionRank.ker_domRestrict_finrank_le line 109
  12. theorem OAI.PerfectCompleteness.BilinearRestrictionRank.rank_domRestrict_add_codim line 122
  13. theorem OAI.PerfectCompleteness.BilinearRestrictionRank.rank_le_rank_comp_add_ker line 132
  14. theorem OAI.PerfectCompleteness.BilinearRestrictionRank.dualRestrict_ker_finrank line 144
  15. theorem OAI.PerfectCompleteness.BilinearRestrictionRank.rank_restrict_add_codim line 149
  16. theorem OAI.PerfectCompleteness.BilinearRestrictionRank.rank_sub_two_codim_le line 160
  17. theorem OAI.PerfectCompleteness.MatrixRowQuotient.exists_section line 181
  18. def OAI.PerfectCompleteness.MatrixRowQuotient.projectMatrix line 185
  19. def OAI.PerfectCompleteness.MatrixRowQuotient.liftMatrix line 189
  20. theorem OAI.PerfectCompleteness.MatrixRowQuotient.projectMatrix_apply line 193
  21. theorem OAI.PerfectCompleteness.MatrixRowQuotient.liftMatrix_apply line 197
  22. theorem OAI.PerfectCompleteness.MatrixRowQuotient.project_lift line 201
  23. theorem OAI.PerfectCompleteness.MatrixRowQuotient.projectMatrix_surjective line 216
  24. theorem OAI.PerfectCompleteness.MatrixRowQuotient.liftMatrix_injective line 222
  25. def OAI.PerfectCompleteness.MatrixRowQuotient.residualVector line 229
  26. theorem OAI.PerfectCompleteness.MatrixRowQuotient.residualVector_val line 240
  27. theorem OAI.PerfectCompleteness.MatrixRowQuotient.subtype_comp_residualVector line 244
  28. theorem OAI.PerfectCompleteness.MatrixRowQuotient.residual_factorization line 248
  29. theorem OAI.PerfectCompleteness.MatrixRowQuotient.project_rankOne line 264
  30. theorem OAI.PerfectCompleteness.MatrixRowQuotient.lift_rankOne line 272
  31. theorem OAI.PerfectCompleteness.MatrixRowQuotient.project_rankOne_of_mem line 280
  32. def OAI.PerfectCompleteness.MatrixSlice.Slice line 307
  33. theorem OAI.PerfectCompleteness.MatrixSlice.domRestrict_translate line 311
  34. theorem OAI.PerfectCompleteness.MatrixSlice.exists_translate_iff line 320
  35. def OAI.PerfectCompleteness.MatrixSlice.parameterEquivSlice line 343
  36. theorem OAI.PerfectCompleteness.MatrixSlice.parameterEquivSlice_val line 355
  37. instance OAI.PerfectCompleteness.MatrixSlice.sliceFintype line 359
  38. instance OAI.PerfectCompleteness.MatrixSlice.sliceNonempty line 363
  39. theorem OAI.PerfectCompleteness.MatrixSlice.expect_translate_eq_slice line 366
  40. theorem OAI.PerfectCompleteness.MatrixSlice.expect_restrict_eq_slice line 373
  41. theorem OAI.PerfectCompleteness.MatrixSlice.domRestrict_eq_iff_basis line 380
  42. def OAI.PerfectCompleteness.MatrixSlice.rowMap line 391
  43. theorem OAI.PerfectCompleteness.MatrixSlice.rowMap_comp_eq_iff line 395
  44. theorem OAI.PerfectCompleteness.MatrixSlice.rowMap_surjective line 411
  45. theorem OAI.PerfectCompleteness.MatrixSlice.exists_translate_iff_equations line 415
  46. theorem OAI.PerfectCompleteness.MatrixSlice.equation_count_eq_order line 424
  47. theorem OAI.PerfectCompleteness.MatrixSlice.column_count_le_order line 429
  48. theorem OAI.PerfectCompleteness.MatrixSlice.row_count_le_order line 432
  49. def OAI.PerfectCompleteness.TensorCosetEvaluation.pureFrequency line 453
  50. theorem OAI.PerfectCompleteness.TensorCosetEvaluation.pureFrequency_tmul line 457
  51. def OAI.PerfectCompleteness.TensorCosetEvaluation.scalarRestriction line 463
  52. theorem OAI.PerfectCompleteness.TensorCosetEvaluation.scalarRestriction_apply line 467
  53. theorem OAI.PerfectCompleteness.TensorCosetEvaluation.scalarRestriction_zero line 470
  54. theorem OAI.PerfectCompleteness.TensorCosetEvaluation.scalarRestriction_add line 476
  55. theorem OAI.PerfectCompleteness.TensorCosetEvaluation.scalarRestriction_sub line 482
  56. theorem OAI.PerfectCompleteness.TensorCosetEvaluation.scalarRestriction_smul line 488
  57. theorem OAI.PerfectCompleteness.TensorCosetEvaluation.scalarRestriction_pure line 494
  58. def OAI.PerfectCompleteness.TensorCosetEvaluation.equationSpace line 502
  59. theorem OAI.PerfectCompleteness.TensorCosetEvaluation.scalarRestriction_mem line 507
  60. theorem OAI.PerfectCompleteness.TensorCosetEvaluation.scalarRestriction_sub_base_mem line 525
  61. theorem OAI.PerfectCompleteness.TensorCosetEvaluation.scalarRestriction_mem_coset_of_eq line 533
  62. theorem OAI.PerfectCompleteness.TensorCosetEvaluation.scalarRestriction_mem_of_vanishes line 542
  63. theorem OAI.PerfectCompleteness.TensorCosetEvaluation.scalarRestriction_factor_mem line 552
  64. theorem OAI.PerfectCompleteness.TensorCosetEvaluation.scalarRestriction_mem_coset_of_factor line 563
  65. theorem OAI.PerfectCompleteness.TensorCosetEvaluation.exists_value_one line 584
  66. theorem OAI.PerfectCompleteness.TensorCosetEvaluation.exists_candidate_restriction line 595
  67. theorem OAI.PerfectCompleteness.TensorCosetEvaluation.annihilator_iff_restriction_zero line 604
  68. theorem OAI.PerfectCompleteness.TensorCosetEvaluation.card_annihilatingCharacters line 607
  69. def OAI.PerfectCompleteness.TensorRestriction.tensorEquivHom line 634
  70. theorem OAI.PerfectCompleteness.TensorRestriction.tensorEquivHom_tmul line 639
  71. def OAI.PerfectCompleteness.TensorRestriction.restrictionMap line 642
  72. theorem OAI.PerfectCompleteness.TensorRestriction.restrictionMap_apply line 646
  73. theorem OAI.PerfectCompleteness.TensorRestriction.restrictionMap_tmul line 650
  74. theorem OAI.PerfectCompleteness.TensorRestriction.restrictionMap_surjective line 654
  75. theorem OAI.PerfectCompleteness.TensorRestriction.fiber_nonempty line 663
  76. theorem OAI.PerfectCompleteness.TensorRestriction.dualMap_injective line 668
  77. theorem OAI.PerfectCompleteness.TensorRestriction.dualMap_ne_zero line 672
  78. def OAI.PerfectCompleteness.TensorRestriction.dualImage line 680
  79. theorem OAI.PerfectCompleteness.TensorRestriction.restrictionMap_tmul_eq_zero line 684
  80. theorem OAI.PerfectCompleteness.TensorRestriction.dualImage_vanishes line 693
  81. theorem OAI.PerfectCompleteness.TensorRestriction.finrank_range line 703
  82. theorem OAI.PerfectCompleteness.TensorRestriction.finrank_dualImage line 710
  83. theorem OAI.PerfectCompleteness.TensorRestriction.finrank_range_le line 717
  84. theorem OAI.PerfectCompleteness.TensorEquationSpace.basis_expansion line 742
  85. theorem OAI.PerfectCompleteness.TensorEquationSpace.mem_equationSpace_of_scalarRestriction_mem line 755
  86. theorem OAI.PerfectCompleteness.TensorEquationSpace.mem_equationSpace_iff line 767
  87. def OAI.PerfectCompleteness.TensorEquationSpace.pureFactor line 782
  88. theorem OAI.PerfectCompleteness.TensorEquationSpace.pureFactor_apply line 789
  89. theorem OAI.PerfectCompleteness.TensorEquationSpace.dualMap_pureFactor line 793
  90. theorem OAI.PerfectCompleteness.TensorEquationSpace.pureFrequency_mem_dualImage line 804
  91. theorem OAI.PerfectCompleteness.TensorEquationSpace.equationSpace_le_dualImage line 809
  92. theorem OAI.PerfectCompleteness.TensorEquationSpace.dualImage_le_equationSpace line 817
  93. theorem OAI.PerfectCompleteness.TensorEquationSpace.dualImage_eq_equationSpace line 825
  94. theorem OAI.PerfectCompleteness.TensorEquationSpace.finrank_equationSpace line 829