recZeroCoe

Mathlib.Algebra.Group.WithOne.Defs

URI: https://scilib.ai/kg/mathlib#WithZero.recZeroCoe

Lean4

/-- Recursor for `WithZero` using the preferred forms `0` and `↑a`. -/
@[elab_as_elim, induction_eliminator, cases_eliminator]
def _root_.WithZero.recZeroCoe {motive : WithZero α → Sort*} (zero : motive 0) (coe : ∀ a : α, motive a) :
    ∀ n : WithZero α, motive n
  | Option.none => zero
  | Option.some x => coe x

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

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

Разделы

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

Аффилиация

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