Documentation

Mathlib.GroupTheory.QuotientGroup.Finite

Deducing finiteness of a group. #

noncomputable def Group.fintypeOfKerLeRange {F G H : Type u} [Group F] [Group G] [Group H] [Fintype F] [Fintype H] (f : F →* G) (g : G →* H) (h : g.ker f.range) :

If F and H are finite such that ker(G →* H) ≤ im(F →* G), then G is finite.

Equations
    Instances For
      noncomputable def AddGroup.fintypeOfKerLeRange {F G H : Type u} [AddGroup F] [AddGroup G] [AddGroup H] [Fintype F] [Fintype H] (f : F →+ G) (g : G →+ H) (h : g.ker f.range) :

      If F and H are finite such that ker(G →+ H) ≤ im(F →+ G), then G is finite.

      Equations
        Instances For
          noncomputable def Group.fintypeOfKerEqRange {F G H : Type u} [Group F] [Group G] [Group H] [Fintype F] [Fintype H] (f : F →* G) (g : G →* H) (h : g.ker = f.range) :

          If F and H are finite such that ker(G →* H) = im(F →* G), then G is finite.

          Equations
            Instances For
              noncomputable def AddGroup.fintypeOfKerEqRange {F G H : Type u} [AddGroup F] [AddGroup G] [AddGroup H] [Fintype F] [Fintype H] (f : F →+ G) (g : G →+ H) (h : g.ker = f.range) :

              If F and H are finite such that ker(G →+ H) = im(F →+ G), then G is finite.

              Equations
                Instances For
                  noncomputable def Group.fintypeOfKerOfCodom {G H : Type u} [Group G] [Group H] [Fintype H] (g : G →* H) [Fintype g.ker] :

                  If ker(G →* H) and H are finite, then G is finite.

                  Equations
                    Instances For
                      noncomputable def AddGroup.fintypeOfKerOfCodom {G H : Type u} [AddGroup G] [AddGroup H] [Fintype H] (g : G →+ H) [Fintype g.ker] :

                      If ker(G →+ H) and H are finite, then G is finite.

                      Equations
                        Instances For
                          noncomputable def Group.fintypeOfDomOfCoker {F G : Type u} [Group F] [Group G] [Fintype F] (f : F →* G) [f.range.Normal] [Fintype (G f.range)] :

                          If F and coker(F →* G) are finite, then G is finite.

                          Equations
                            Instances For
                              noncomputable def AddGroup.fintypeOfDomOfCoker {F G : Type u} [AddGroup F] [AddGroup G] [Fintype F] (f : F →+ G) [f.range.Normal] [Fintype (G f.range)] :

                              If F and coker(F →+ G) are finite, then G is finite.

                              Equations
                                Instances For