Documentation
Atlas
.
NumberTheoryI
.
code
.
Cor2361
Search
return to top
source
Imports
Init
Mathlib.Algebra.Category.ModuleCat.Basic
Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
Imported by
corollary_23_61
source
instance
corollary_23_61
{
R
:
Type
u}
[
Ring
R
]
(
A
:
ModuleCat
R
)
:
(
CategoryTheory.preadditiveYoneda
.
obj
A
)
.
Additive