OAI/LinearAlgebra/MatrixMultiplication/Recovery/InheritedOrbitProfiles.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Finite orbit symmetries, masks and exact recovery operations.

  1. abbrev OAI.MatrixMultiplication.PermutationMatching.PairProfile line 18
  2. def OAI.MatrixMultiplication.PermutationMatching.pairProfile line 21
  3. theorem OAI.MatrixMultiplication.PermutationMatching.pairProfile_smul line 24
  4. theorem OAI.MatrixMultiplication.PermutationMatching.completeWordPair_ext line 37
  5. theorem OAI.MatrixMultiplication.PermutationMatching.pairProfile_eq_iff line 45
  6. theorem OAI.MatrixMultiplication.PermutationMatching.pairProfile_eq_iff_orbitRel line 65
  7. abbrev OAI.MatrixMultiplication.PermutationMatching.PairOrbit line 75
  8. def OAI.MatrixMultiplication.PermutationMatching.pairOrbitProfile line 78
  9. theorem OAI.MatrixMultiplication.PermutationMatching.pairOrbitProfile_injective line 81
  10. theorem OAI.MatrixMultiplication.PermutationMatching.card_pairOrbits_le line 94
  11. theorem OAI.MatrixMultiplication.PermutationMatching.card_pairOrbits_le_common_bound line 108