coeFnAddMonoidHom

Mathlib.Algebra.DirectSum.Basic

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

← MathLib Explorer

English

Compatibility with scalar action on the first component.

Русский

Совместимость с действием скаляра на первый компонент.

LaTeX

$$$gMul(a, s\\cdot b) = s\\cdot gMul(a,b)$$$

Lean4

/-- Coercion from a `DirectSum` to a pi type is an `AddMonoidHom`. -/
def coeFnAddMonoidHom [∀ i, AddCommMonoid (β i)] : (⨁ i, β i) →+ (Π i, β i)
    where
  toFun x := x
  __ := DFinsupp.coeFnAddMonoidHom

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

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

Разделы

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

Аффилиация

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