OAI/Algebra/Finitistic/Ordinary/OrdinaryOffDiagonalProjective.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.inflatedPair line 13
2. def OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.rightPairEquiv line 19
3. theorem OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.right_projective line 29

   Source documentation

   Off-diagonal right projectivity follows from the actual two product-factor modules.

   theorem right_projective [Module.Projective Lᵐᵒᵖ O] [Module.Projective Rᵐᵒᵖ T] :
       Module.Projective (L × R)ᵐᵒᵖ (OffDiagonal O T) := by
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal