The category of finite additive groups.
Instances For
Equations
- FiniteGrp.instCoeSortType = { coe := fun (G : FiniteGrp.{?u.1}) => ↑G.toGrp }
Equations
- FiniteAddGrp.instCoeSortType = { coe := fun (G : FiniteAddGrp.{?u.1}) => ↑G.toAddGrp }
Equations
- G.instGroupαToGrp = inferInstanceAs (Group ↑G.toGrp)
Equations
- G.instGroupαToAddGrp = inferInstanceAs (AddGroup ↑G.toAddGrp)
Equations
- G.instFunLikeHomαGroupToGrp H = inferInstanceAs (FunLike (↑G.toGrp →* ↑H.toGrp) ↑G.toGrp ↑H.toGrp)
Equations
- G.instFunLikeHomαAddGroupToAddGrp H = inferInstanceAs (FunLike (↑G.toAddGrp →+ ↑H.toAddGrp) ↑G.toAddGrp ↑H.toAddGrp)
instance
FiniteGrp.instMonoidHomClassHomαGroupToGrp
(G H : FiniteGrp.{u_1})
:
MonoidHomClass (G ⟶ H) ↑G.toGrp ↑H.toGrp
instance
FiniteAddGrp.instAddMonoidHomClassHomαAddGroupToAddGrp
(G H : FiniteAddGrp.{u_1})
:
AddMonoidHomClass (G ⟶ H) ↑G.toAddGrp ↑H.toAddGrp
Construct a term of FiniteGrp
from a type endowed with the structure of a finite group.
Equations
- FiniteGrp.of G = FiniteGrp.mk (Grp.of G)
Instances For
Construct a term of FiniteAddGrp
from a type endowed with the structure of a
finite additive group.
Equations
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
Equations
Instances For
theorem
FiniteGrp.ofHom_apply
{X Y : Type u}
[Group X]
[Finite X]
[Group Y]
[Finite Y]
(f : X →* Y)
(x : X)
:
(FiniteGrp.ofHom f) x = f x
theorem
FiniteAddGrp.ofHom_apply
{X Y : Type u}
[AddGroup X]
[Finite X]
[AddGroup Y]
[Finite Y]
(f : X →+ Y)
(x : X)
:
(FiniteAddGrp.ofHom f) x = f x