Documentation
Mathlib
.
Algebra
.
Group
.
TypeTags
.
Finite
Search
return to top
source
Imports
Init
Mathlib.Data.Finite.Defs
Mathlib.Algebra.Group.TypeTags.Basic
Imported by
instFiniteAdditive
instFiniteMultiplicative
instInfiniteAdditive
instInfiniteMultiplicative
Finite
and
Infinite
are preserved by
Additive
and
Multiplicative
.
#
source
instance
instFiniteAdditive
{α :
Type
u}
[
Finite
α
]
:
Finite
(
Additive
α
)
source
instance
instFiniteMultiplicative
{α :
Type
u}
[
Finite
α
]
:
Finite
(
Multiplicative
α
)
source
instance
instInfiniteAdditive
{α :
Type
u}
[h :
Infinite
α
]
:
Infinite
(
Additive
α
)
source
instance
instInfiniteMultiplicative
{α :
Type
u}
[h :
Infinite
α
]
:
Infinite
(
Multiplicative
α
)