Documentation

Mathlib.Algebra.Category.Grp.FiniteGrp

Main definitions and results #

structure FiniteGrp :
Type (u_1 + 1)

The category of finite groups.

  • toGrp : Grp

    A group that is finite

  • isFinite : Finite self.toGrp
Instances For
    structure FiniteAddGrp :
    Type (u_1 + 1)

    The category of finite additive groups.

    • toAddGrp : AddGrp

      An add group that is finite

    • isFinite : Finite self.toAddGrp
    Instances For
      Equations
      Equations
      instance FiniteGrp.instFunLikeHomαGroupToGrp (G H : FiniteGrp.{u_1}) :
      FunLike (G H) G.toGrp H.toGrp
      Equations
      instance FiniteAddGrp.instFunLikeHomαAddGroupToAddGrp (G H : FiniteAddGrp.{u_1}) :
      FunLike (G H) G.toAddGrp H.toAddGrp
      Equations

      Construct a term of FiniteGrp from a type endowed with the structure of a finite group.

      Equations
      Instances For

        Construct a term of FiniteAddGrp from a type endowed with the structure of a finite additive group.

        Equations
        Instances For
          def FiniteGrp.ofHom {X Y : Type u} [Group X] [Finite X] [Group Y] [Finite Y] (f : X →* Y) :

          The morphism in FiniteGrp, induced from a morphism of the category Grp.

          Equations
          Instances For

            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) :