Theorems · Theorem · group theory

HNNExtension.NormalWord.prod_smul

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

Defined in: Mathlib.GroupTheory.HNNExtension
Cited by: 1 results in Mathlib
Foundations: Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Group

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites23

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Groupstatement and proof · cited by 6,238
Subgroupstatement and proof · cited by 3,593
mul_assocproof · cited by 1,667
MulEquivstatement and proof · cited by 1,142
pow_oneproof · cited by 894
SemigroupAction.mul_smulproof · cited by 291
zpow_ofNatproof · cited by 144
mul_inv_cancel_leftproof · cited by 86
smul_inv_smulproof · cited by 53
HNNExtension.NormalWord.TransversalPairstatement and proof · cited by 46
HNNExtension.NormalWordstatement and proof · cited by 36

Cited by1

Results whose statement or proof uses this declaration.

HNNExtension.ReducedWord.exists_normalWord_prod_eqproof · cited by 1