PDSimpleTensor.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.PDTensor.right_simple_annihilated line 14
Source documentation
For an Artinian ring the left-defined ring radical annihilates every actual simple right module. The proof uses cyclicity and a genuine inverse; it does not assume a left/right-radical identification theorem.
```
theorem right_simple_annihilated [IsArtinianRing A]
    (U : Type u) [AddCommGroup U] [Module Aᵐᵒᵖ U] [IsSimpleModule Aᵐᵒᵖ U]
    (a : A) (ha : a ∈ Ring.jacobson A) (u : U) : MulOpposite.op a • u=0 := by
…
```
def OAI.LittleFinitistic.PDTensor.simpleTorIsoTerm line 46
Source documentation
The derived tensor with every actual simple right module is the tensor of that simple module with the n-th minimal projective-resolution term.
```
def simpleTorIsoTerm (n : ℕ) : Tor (k := k) U M.cat n ≅
…
```
Mentions: OAI.LittleFinitistic.PDTensor.Tor