OAI/Algebra/Finitistic/Ordinary/OrdinaryTensorIdealActions.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.OrdinarySimulation.TensorIdeal.coefficient line 11
2. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorIdeal.coefficient_commute line 13
3. def OAI.LittleFinitistic.OrdinarySimulation.TensorIdeal.leftMultiply line 18
4. def OAI.LittleFinitistic.OrdinarySimulation.TensorIdeal.leftAction line 26
5. instance OAI.LittleFinitistic.OrdinarySimulation.TensorIdeal.leftModule line 47
6. instance OAI.LittleFinitistic.OrdinarySimulation.TensorIdeal.towerLeft line 50
7. instance OAI.LittleFinitistic.OrdinarySimulation.TensorIdeal.commute line 56
8. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorIdeal.left_smul_value line 60