OAI/Algebra/Finitistic/Ordinary/OrdinaryFirstBlockTensor.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.OrdinarySimulation.FirstBlockTensor.source line 15
2. abbrev OAI.LittleFinitistic.OrdinarySimulation.FirstBlockTensor.target line 16
3. def OAI.LittleFinitistic.OrdinarySimulation.FirstBlockTensor.forward line 18
4. def OAI.LittleFinitistic.OrdinarySimulation.FirstBlockTensor.inverse line 25
5. theorem OAI.LittleFinitistic.OrdinarySimulation.FirstBlockTensor.other_block_zero line 43
6. theorem OAI.LittleFinitistic.OrdinarySimulation.FirstBlockTensor.inverse_forward line 56
7. theorem OAI.LittleFinitistic.OrdinarySimulation.FirstBlockTensor.forward_inverse line 73
8. def OAI.LittleFinitistic.OrdinarySimulation.FirstBlockTensor.equivalence line 82

   Source documentation

   Tensor on the first block selects O and has its actual output on the second block.

   def equivalence : source k L R O T Z ≃ₗ[L × R] target k L R O Z where
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.FirstBlockTensor.source, OAI.LittleFinitistic.OrdinarySimulation.FirstBlockTensor.target