Theorems · Definition · group theory

HNNExtension.NormalWord.ReducedWord.prod

{G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} → (φ : ↥A ≃* ↥B) → HNNExtension.NormalWord.ReducedWord G A B → HNNExtension G A B φ

The product of a ReducedWord as an element of the HNNExtension

Defined in

Mathlib.GroupTheory.HNNExtension

Cited by

10 results in Mathlib

Foundations

Depth 56 from the axioms · uses propext, Quot.sound

Assumes

Group