smulZeroClass

Mathlib.Algebra.GroupWithZero.Action.Pi

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

Lean4

instance smulZeroClass (α) {n : ∀ i, Zero <| f i} [∀ i, SMulZeroClass α <| f i] :
    @SMulZeroClass α (∀ i : I, f i) (@Pi.instZero I f n) where smul_zero _ := funext fun _ => smul_zero _

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

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

Разделы

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

Аффилиация

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