Theorems · Theorem · group theory

HNNExtension.NormalWord.of_smul_eq_smul

∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B}
  (g : G) (w : HNNExtension.NormalWord d), HNNExtension.of g • w = g • w

Defined in

Mathlib.GroupTheory.HNNExtension

Cited by

4 results in Mathlib

Foundations

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

Assumes

Group