Theorems · Definition · group theory

QuotientAddGroup.equivQuotientAddSubgroupOfOfEq

{G : Type u} →
  [inst : AddGroup G] →
    {A' A B' B : AddSubgroup G} →
      [hAN : (A'.addSubgroupOf A).Normal] →
        [hBN : (B'.addSubgroupOf B).Normal] → A' = B' → A = B → ↥A ⧸ A'.addSubgroupOf A ≃+ ↥B ⧸ B'.addSubgroupOf 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'.addSubgroupOf A : AddSubgroup 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

AddGroupAddSubgroup.NormalAddSubgroup.Normal