OAI/Computability/DeterministicSum/TensorEncoding.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Digit encodings for tensor transforms.

  1. def OAI.DeterministicThreeSum.Structured.Indexed.Axis.digitCode line 13
  2. lemma OAI.DeterministicThreeSum.Structured.Indexed.Axis.digitCode_lt line 17
  3. def OAI.DeterministicThreeSum.Structured.Indexed.Axis.digitCoefficient line 27
  4. theorem OAI.DeterministicThreeSum.Structured.Indexed.Axis.tensorValue_eq_tensor line 31
  5. theorem OAI.DeterministicThreeSum.Structured.Indexed.Axis.tensorCommand_tensor_correct line 67