OAI/LinearAlgebra/MatrixMultiplication/Recovery/EquivOrbitTransport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite orbit symmetries, masks and exact recovery operations.

  1. def OAI.MatrixMultiplication.EquivOrbitTransport.action line 14
  2. theorem OAI.MatrixMultiplication.EquivOrbitTransport.equiv_smul line 23
  3. theorem OAI.MatrixMultiplication.EquivOrbitTransport.orbitSet_map line 32
  4. theorem OAI.MatrixMultiplication.EquivOrbitTransport.orbitSet_card line 41
  5. theorem OAI.MatrixMultiplication.EquivOrbitTransport.rejected_card line 48
  6. theorem OAI.MatrixMultiplication.EquivOrbitTransport.rejected_fraction line 59
  7. theorem OAI.MatrixMultiplication.EquivOrbitTransport.coefficients_preserved line 70