Theorems · Definition · group theory

FiniteIndexNormalSubgroup.mk.noConfusion

{G : Type u_1} →
  {inst : Group G} →
    {P : Sort u} →
      {toSubgroup : Subgroup G} →
        {isNormal' : autoParam toSubgroup.Normal FiniteIndexNormalSubgroup.isNormal'._autoParam} →
          {isFiniteIndex' : autoParam toSubgroup.FiniteIndex FiniteIndexNormalSubgroup.isFiniteIndex'._autoParam} →
            {toSubgroup' : Subgroup G} →
              {isNormal'' : autoParam toSubgroup'.Normal FiniteIndexNormalSubgroup.isNormal'._autoParam} →
                {isFiniteIndex'' :
                    autoParam toSubgroup'.FiniteIndex FiniteIndexNormalSubgroup.isFiniteIndex'._autoParam} →
                  { toSubgroup := toSubgroup, isNormal' := isNormal', isFiniteIndex' := isFiniteIndex' } =
                      { toSubgroup := toSubgroup', isNormal' := isNormal'', isFiniteIndex' := isFiniteIndex'' } →
                    (toSubgroup ≍ toSubgroup' → P) → P

Defined in

Mathlib.GroupTheory.FiniteIndexNormalSubgroup

Cited by

1 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms