Equations
- FiniteGrp.instCoeSortType = { coe := fun (G : FiniteGrp.{?u.1}) => ↑G.toGrp }
Equations
- FiniteAddGrp.instCoeSortType = { coe := fun (G : FiniteAddGrp.{?u.1}) => ↑G.toAddGrp }
Construct a term of FiniteGrp
from a type endowed with the structure of a finite group.
Instances For
Construct a term of FiniteAddGrp
from a type endowed with the structure of a
finite additive group.
Instances For
def
FiniteAddGrp.ofHom
{X Y : Type u}
[AddGroup X]
[Finite X]
[AddGroup Y]
[Finite Y]
(f : X →+ Y)
:
The morphism in FiniteAddGrp
, induced from a morphism of the category AddGrp