Theorems · Definition · group theory

Monoid.CoprodI.Word.casesOn

{ι : Type u_1} →
  {M : ι → Type u_2} →
    [inst : (i : ι) → Monoid (M i)] →
      {motive : Monoid.CoprodI.Word M → Sort u} →
        (t : Monoid.CoprodI.Word M) →
          ((toList : List ((i : ι) × M i)) →
              (ne_one : ∀ l ∈ toList, l.snd ≠ 1) →
                (chain_ne : List.IsChain (fun l l' => l.fst ≠ l'.fst) toList) →
                  motive { toList := toList, ne_one := ne_one, chain_ne := chain_ne }) →
            motive t

Defined in: Mathlib.GroupTheory.CoprodI
Cited by: 3 results in Mathlib
Foundations: Depth 8 from the axioms · uses no axioms
Assumes: Monoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites2

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

Monoidstatement and proof · cited by 3,887
Monoid.CoprodI.Wordstatement and proof · cited by 55

Cited by6

Results whose statement or proof uses this declaration.

Monoid.CoprodI.Word.consRecOnproof · cited by 6
Monoid.CoprodI.NeWord.of_wordproof · cited by 1
Monoid.PushoutI.NormalWord.extproof · cited by 1
Monoid.CoprodI.Word.noConfusionproof · cited by 0
Monoid.CoprodI.Word.noConfusionTypeproof · cited by 0
Monoid.CoprodI.Word.mem_smul_iffproof · cited by 0