Documentation
AlgebraInLean
.
Chapter01
.
Sheet05
Search
Google site search
return to top
source
Imports
Init
AlgebraInLean.Chapter01.Sheet04
Imported by
AlgebraInLean
.
instAbelianGroupFinOfNeZeroNat
source
instance
AlgebraInLean
.
instAbelianGroupFinOfNeZeroNat
(n :
ℕ
)
[
NeZero
n
]
:
AlgebraInLean.AbelianGroup
(
Fin
n
)
Equations
AlgebraInLean.instAbelianGroupFinOfNeZeroNat
n
=
AlgebraInLean.AbelianGroup.mk
⋯