addMonoidWithOne

Mathlib.Algebra.Ring.Pi

URI: https://scilib.ai/kg/mathlib#Pi.addMonoidWithOne

Lean4

instance addMonoidWithOne [∀ i, AddMonoidWithOne (f i)] : AddMonoidWithOne (∀ i, f i)
    where
  natCast n _ := n
  natCast_zero := funext fun _ ↦ AddMonoidWithOne.natCast_zero
  natCast_succ n := funext fun _ ↦ AddMonoidWithOne.natCast_succ n

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

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

Разделы

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

Аффилиация

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