recOneCoe

Mathlib.Algebra.Group.WithOne.Defs

URI: https://scilib.ai/kg/mathlib#WithOne.recOneCoe

Lean4

/-- Recursor for `WithOne` using the preferred forms `1` and `↑a`. -/
@[to_additive existing, elab_as_elim, induction_eliminator, cases_eliminator]
def recOneCoe {motive : WithOne α → Sort*} (one : motive 1) (coe : ∀ a : α, motive a) : ∀ n : WithOne α, motive n
  | Option.none => one
  | Option.some x => coe x

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

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

Разделы

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

Аффилиация

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