OAI/Algebra/Finitistic/Ordinary/OrdinaryProductSplitting.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.ProductModules.secondInflation line 13
2. abbrev OAI.LittleFinitistic.ProductModules.swapModule line 16
3. abbrev OAI.LittleFinitistic.ProductModules.secondObject line 19
4. abbrev OAI.LittleFinitistic.ProductModules.pairObject line 22
5. def OAI.LittleFinitistic.ProductModules.splitTo line 27
6. def OAI.LittleFinitistic.ProductModules.joinTo line 51
7. def OAI.LittleFinitistic.ProductModules.splitting line 65

   Source documentation

   Every module over a product ring splits into its two actual central-idempotent components.

   def splitting : M ≃ₗ[L × R] pairObject L R M where
   …

   Mentions: OAI.LittleFinitistic.ProductModules.pairObject