recOnMul

Mathlib.Algebra.Free

URI: https://scilib.ai/kg/mathlib#FreeSemigroup.recOnMul

Lean4

/-- Recursor for free semigroup using `of` and `*`. -/
@[to_additive (attr := elab_as_elim, induction_eliminator) /--
    Recursor for free additive semigroup using `of` and `+`. -/
    ]
protected def recOnMul {C : FreeSemigroup α → Sort l} (x) (ih1 : ∀ x, C (of x))
    (ih2 : ∀ x y, C (of x) → C y → C (of x * y)) : C x :=
  FreeSemigroup.recOn x fun f s ↦ List.recOn s ih1 (fun hd tl ih f ↦ ih2 f ⟨hd, tl⟩ (ih1 f) (ih hd)) f

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru