OAI/LinearAlgebra/MatrixMultiplication/Completion/Cardinality.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Readable tensor completion and its finite arithmetic realization.

  1. def OAI.MatrixMultiplication.CompletionCardinality.conditionalCount line 19
  2. abbrev OAI.MatrixMultiplication.CompletionCardinality.AllowedLeaf line 23
  3. def OAI.MatrixMultiplication.CompletionCardinality.centerLeafEquiv line 26
  4. def OAI.MatrixMultiplication.CompletionCardinality.noncenterLeafEquiv line 34
  5. def OAI.MatrixMultiplication.CompletionCardinality.allCenterEquiv line 62
  6. theorem OAI.MatrixMultiplication.CompletionCardinality.card_allowedLeaf line 75
  7. theorem OAI.MatrixMultiplication.CompletionCardinality.count_complete_center line 83
  8. theorem OAI.MatrixMultiplication.CompletionCardinality.count_complete_noncenter line 91
  9. theorem OAI.MatrixMultiplication.CompletionCardinality.count_complete line 114