Theorems · Theorem · group theory

Monoid.PushoutI.NormalWord.base_smul_def

∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [inst_2 : DecidableEq ι]
  [inst_3 : (i : ι) → DecidableEq (G i)] (h : H) (w : Monoid.PushoutI.NormalWord d),
  (Monoid.PushoutI.base φ) h • w = { toWord := w.toWord, head := h * w.head, normalized := ⋯ }

Defined in

Mathlib.GroupTheory.PushoutI

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupGroupDecidableEqDecidableEq