OAI/Algebra/Finitistic/Selected/SelectedPDResidueProjection.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.SelectedPDDetection.augmentation_surjective line 10
2. theorem OAI.LittleFinitistic.SelectedPDDetection.augmentation_kernel_square_zero line 13
3. def OAI.LittleFinitistic.SelectedPDDetection.rightResidueEquiv line 18

   Source documentation

   The detector's canonical residue is the right D-residue inflated along A → D.

   def rightResidueEquiv : PDTensor.Residue (A := A) ≃ₗ[Aᵐᵒᵖ]
   …

   Mentions: OAI.LittleFinitistic.PDTensor.Residue

4. def OAI.LittleFinitistic.SelectedPDDetection.residueTorIso line 22
5. theorem OAI.LittleFinitistic.SelectedPDDetection.pdLE_iff_inflated_D_residueTor line 28