Theorems · Theorem · group theory

Subgroup.leftTransversals.smul_diff_smul

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

Defined in

Mathlib.GroupTheory.Transfer

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupCommGroupSubgroup.FiniteIndex