Theorems · Theorem · group theory

Subgroup.leftTransversals.diff_mul_diff

∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {A : Type u_2} [inst_1 : CommGroup A] (ϕ : ↥H →* A)
  (R S T : H.LeftTransversal) [inst_2 : H.FiniteIndex],
  Subgroup.leftTransversals.diff ϕ R S * Subgroup.leftTransversals.diff ϕ S T = Subgroup.leftTransversals.diff ϕ R T

Defined in

Mathlib.GroupTheory.Transfer

Cited by

3 results in Mathlib

Foundations

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

Assumes

GroupCommGroupSubgroup.FiniteIndex