OAI/LinearAlgebra/MatrixFields/Parameters/JointPopulation.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MatrixAllFields.MatrixMultiplication.JointPopulation.HistoryKey line 21
  2. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointPopulation.Shape line 28
  3. def OAI.MatrixAllFields.MatrixMultiplication.JointPopulation.shapeSide line 30
  4. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointPopulation.Positions line 36
  5. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointPopulation.Target line 37
  6. def OAI.MatrixAllFields.MatrixMultiplication.JointPopulation.canonicalTarget line 39
  7. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulation.target_card line 42
  8. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulation.target_nonempty line 47
  9. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointPopulation.Position line 49
  10. def OAI.MatrixAllFields.MatrixMultiplication.JointPopulation.triple line 51
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulation.triple_injective line 57
  12. def OAI.MatrixAllFields.MatrixMultiplication.JointPopulation.targetSet line 68
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulation.targetSet_card line 71
  14. abbrev OAI.MatrixAllFields.MatrixMultiplication.JointPopulation.Class line 76
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulation.class_card line 80
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulation.symbol_count_pos line 84
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulation.triple_support line 90
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulation.exists_position_permutation line 98
  19. def OAI.MatrixAllFields.MatrixMultiplication.JointPopulation.sideWord line 108
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulation.sideWord_triple line 113
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulation.marginal_population_eq line 117
  22. def OAI.MatrixAllFields.MatrixMultiplication.JointPopulation.ambientSet line 124
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.JointPopulation.targetSet_subset_ambient line 130