Theorems · Definition · group theory

Subgroup.leftTransversals.diff

{G : Type u_1} →
  [inst : Group G] →
    {H : Subgroup G} →
      {A : Type u_2} → [inst_1 : CommGroup A] → (↥H →* A) → H.LeftTransversal → H.LeftTransversal → [H.FiniteIndex] → A

The difference of two left transversals

Defined in

Mathlib.GroupTheory.Transfer

Cited by

8 results in Mathlib

Foundations

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

Assumes

GroupCommGroupSubgroup.FiniteIndex