Theorems · Definition · group theory

FreeAddMonoid.recOn

{α : Type u_1} →
  {motive : FreeAddMonoid α → Sort u_6} →
    (xs : FreeAddMonoid α) →
      motive 0 → ((x : α) → (xs : FreeAddMonoid α) → motive xs → motive (FreeAddMonoid.of x + xs)) → motive xs

Recursor for FreeAddMonoid using 0 and FreeAddMonoid.of x + xs instead of [] and x :: xs.

Defined in

Mathlib.Algebra.FreeMonoid.Basic

Cited by

8 results in Mathlib

Foundations

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