OAI/Algebra/Finitistic/Ordinary/OrdinarySecondBlockTensor.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

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

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

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