instNatCastOfNat

Mathlib.Algebra.DirectSum.Ring

URI: https://scilib.ai/kg/mathlib#DirectSum.instNatCastOfNat

Lean4

instance : NatCast (A 0) :=
  ⟨GSemiring.natCast⟩
    -- TODO: These could be replaced by the general lemmas for `AddMonoidHomClass` (`map_natCast'` and
    -- `map_ofNat'`) if those were marked `@[simp low]`.

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

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

Разделы

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

Аффилиация

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