OAI/Computability/DeterministicSum/MatrixProduct.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Charged scalar leaves and exact source bilinear product assembly.

  1. def OAI.DeterministicThreeSum.Structured.MatrixLeaves.body line 11
  2. theorem OAI.DeterministicThreeSum.Structured.MatrixLeaves.body_correct line 18
  3. def OAI.DeterministicThreeSum.Structured.MatrixLeaves.command line 49
  4. theorem OAI.DeterministicThreeSum.Structured.MatrixLeaves.command_correct line 51
  5. lemma OAI.DeterministicThreeSum.Structured.MatrixLeaves.value_modular line 89
  6. lemma OAI.DeterministicThreeSum.Structured.Indexed.MatrixUp.value_succ_last line 97
  7. theorem OAI.DeterministicThreeSum.Structured.Indexed.MatrixUp.value_multiplyBatch line 111
  8. theorem OAI.DeterministicThreeSum.Structured.Indexed.MatrixUp.value_product line 142