PDAllSimples.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.PDTensor.exists_simple_tensor_nonzero line 15
Source documentation
A nonzero finite module is detected by tensor with an actual simple right submodule of A/rad A. This is an existence proof, not an assumed simple detector.
```
theorem exists_simple_tensor_nonzero
    (N : Type u) [AddCommGroup N] [Module k N] [Module A N] [IsScalarTower k A N]
    [Module.Finite A N] [Nontrivial N] :
    ∃ S : Submodule Aᵐᵒᵖ (Residue (A := A)), IsSimpleModule Aᵐᵒᵖ S ∧
…
```
Mentions: OAI.LittleFinitistic.PDTensor.Residue
theorem OAI.LittleFinitistic.PDTensor.pdLE_iff_simpleTor_zero line 56
Source documentation
The exact simple-module form of projective-dimension detection. The test modules here are actual simple right submodules of the fixed radical quotient.
```
theorem pdLE_iff_simpleTor_zero (n : ℕ) :
    HasProjectiveDimensionLE M.cat n ↔
      ∀ S : Submodule Aᵐᵒᵖ (Residue (A := A)), IsSimpleModule Aᵐᵒᵖ S →
…
```
Mentions: OAI.LittleFinitistic.PDTensor.Residue