Theorems · Definition · group theory

Monoid.PushoutI.NormalWord.cons

{ι : 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 φ} →
              {i : ι} →
                (g : G i) →
                  (w : Monoid.PushoutI.NormalWord d) →
                    w.fstIdx ≠ some i → g ∉ (φ i).range → Monoid.PushoutI.NormalWord d

A constructor that multiplies a NormalWord by an element, with condition to make sure the underlying list does get longer.

Defined in

Mathlib.GroupTheory.PushoutI

Cited by

7 results in Mathlib

Foundations

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

Assumes

GroupGroup