Theorems · Definition · group theory

QuotientGroup.equivQuotientSubgroupOfOfEq

{G : Type u} →
  [inst : Group G] →
    {A' A B' B : Subgroup G} →
      [hAN : (A'.subgroupOf A).Normal] →
        [hBN : (B'.subgroupOf B).Normal] → A' = B' → A = B → ↥A ⧸ A'.subgroupOf A ≃* ↥B ⧸ B'.subgroupOf B

Let A', A, B', B be subgroups of G. If A' = B' and A = B, then the quotients A / (A' ⊓ A) and B / (B' ⊓ B) are isomorphic. Applying this equiv is nicer than rewriting along the equalities, since the type of (A'.subgroupOf A : Subgroup A) depends on A.

Defined in

Mathlib.GroupTheory.QuotientGroup.Basic

Cited by

0 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupSubgroup.NormalSubgroup.Normal