Theorems · Inductive type · group theory

Monoid.CoprodI.NeWord

{ι : Type u_1} → (M : ι → Type u_2) → [(i : ι) → Monoid (M i)] → ι → ι → Type (max u_1 u_2)

A NeWord M i j is a representation of a non-empty reduced words where the first letter comes from M i and the last letter comes from M j. It can be constructed from singletons and via concatenation, and thus provides a useful induction principle.

Defined in

Mathlib.GroupTheory.CoprodI

Cited by

36 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

Monoid