Theorems · Theorem · group theory

HNNExtension.NormalWord.unitsSMul_neg

∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B}
  (u : ℤˣ) (w : HNNExtension.NormalWord d),
  HNNExtension.NormalWord.unitsSMul φ (-u) (HNNExtension.NormalWord.unitsSMul φ u w) = w

Defined in

Mathlib.GroupTheory.HNNExtension

Cited by

0 results in Mathlib

Foundations

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

Assumes

Group