OAI/Algebra/Finitistic/Ordinary/OrdinaryProductOpposite.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.ProductModules.oppositeEquiv line 12

   Source documentation

   The opposite of the actual product ring is the product of the two opposite rings.

   def oppositeEquiv : (L × R)ᵐᵒᵖ ≃+* Lᵐᵒᵖ × Rᵐᵒᵖ where
   …

2. abbrev OAI.LittleFinitistic.ProductModules.oppositeModule line 20
3. def OAI.LittleFinitistic.ProductModules.oppositeModuleEquiv line 25
4. theorem OAI.LittleFinitistic.ProductModules.opposite_product_module_bound line 36