Theorems · Definition · group theory

FreeMonoid.recOn

{α : Type u_1} →
  {motive : FreeMonoid α → Sort u_6} →
    (xs : FreeMonoid α) →
      motive 1 → ((x : α) → (xs : FreeMonoid α) → motive xs → motive (FreeMonoid.of x * xs)) → motive xs

Recursor for FreeMonoid using 1 and FreeMonoid.of x * xs instead of [] and x :: xs.

Defined in

Mathlib.Algebra.FreeMonoid.Basic

Cited by

7 results in Mathlib

Foundations

Depth 39 from the axioms · uses propext, Quot.sound