Documentation
Atlas
.
NumberTheoryI
.
code
.
Lem2378
Search
return to top
source
Imports
Init
Mathlib.CategoryTheory.Abelian.LeftDerived
Mathlib.CategoryTheory.Monoidal.Tor
Mathlib.Algebra.Category.ModuleCat.Abelian
Mathlib.Algebra.Category.ModuleCat.Projective
Mathlib.CategoryTheory.Abelian.Projective.Resolution
Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
Imported by
lemma_23_78
source
noncomputable def
lemma_23_78
(
R
:
Type
u)
[
CommRing
R
]
(
M
A
:
ModuleCat
R
)
:
(
(
CategoryTheory.Tor
(
ModuleCat
R
)
0
)
.
obj
M
)
.
obj
A
≅
CategoryTheory.MonoidalCategoryStruct.tensorObj
M
A
Instances For