Theorems · Definition · group theory

Monoid.PushoutI.NormalWord.consRecOn

{ι : 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)] →
                  {motive : Monoid.PushoutI.NormalWord d → Sort u_5} →
                    (w : Monoid.PushoutI.NormalWord d) →
                      motive Monoid.PushoutI.NormalWord.empty →
                        ((i : ι) →
                            (g : G i) →
                              (w : Monoid.PushoutI.NormalWord d) →
                                (hmw : w.fstIdx ≠ some i) →
                                  g ∈ d.set i →
                                    (hgr : g ∉ (φ i).range) →
                                      w.head = 1 → motive w → motive (Monoid.PushoutI.NormalWord.cons g w hmw hgr)) →
                          ((h : H) →
                              (w : Monoid.PushoutI.NormalWord d) →
                                w.head = 1 → motive w → motive ((Monoid.PushoutI.base φ) h • w)) →
                            motive w

Induction principle for NormalWord, that corresponds closely to inducting on the underlying list.

Defined in

Mathlib.GroupTheory.PushoutI

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupGroupDecidableEqDecidableEq