OAI/LinearAlgebra/MatrixMultiplication/Duality/Uniform.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Dual matrix multiplication exponents and finite rectangular constructions.

  1. structure OAI.MatrixMultiplication.DualUniform.UniformLaws line 23
  2. theorem OAI.MatrixMultiplication.DualUniform.UniformLaws.color line 28
  3. theorem OAI.MatrixMultiplication.DualUniform.UniformLaws.entropy_B line 37
  4. theorem OAI.MatrixMultiplication.DualUniform.UniformLaws.entropy_A line 42
  5. theorem OAI.MatrixMultiplication.DualUniform.UniformLaws.entropy_C line 47
  6. theorem OAI.MatrixMultiplication.DualUniform.conditionalCompletionLaw_uniform_common line 52
  7. theorem OAI.MatrixMultiplication.DualUniform.inactive_uniform_update line 66
  8. theorem OAI.MatrixMultiplication.DualUniform.minusLaws_uniform line 82
  9. theorem OAI.MatrixMultiplication.DualUniform.plusALaws_uniform line 100
  10. theorem OAI.MatrixMultiplication.DualUniform.plusCLaws_uniform line 115
  11. theorem OAI.MatrixMultiplication.DualUniform.pure_map_mass line 130
  12. theorem OAI.MatrixMultiplication.DualUniform.baseLaws_uniform line 139