instInhabitedAlgebra

Mathlib.CategoryTheory.Monad.Algebra

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Monad.instInhabitedAlgebra

Lean4

instance [Inhabited C] : Inhabited (Algebra T) :=
  ⟨(free T).obj default⟩
    -- The other two `simps` projection lemmas can be derived from these two, so `simp_nf` complains if
    -- those are added too

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

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

Разделы

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

Аффилиация

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