OAI/Algebra/Finitistic/Dimension/PDResidueSemisimple.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.PDTensor.residue_semisimple line 14

   Source documentation

   The actual residue right module is semisimple.

   theorem residue_semisimple : IsSemisimpleModule Aᵐᵒᵖ (Residue (A := A)) := by
   …

   Mentions: OAI.LittleFinitistic.PDTensor.Residue