mapDMatrix

Mathlib.Data.Matrix.DMatrix

URI: https://scilib.ai/kg/mathlib#AddMonoidHom.mapDMatrix

Lean4

/-- The `AddMonoidHom` between spaces of dependently typed matrices
induced by an `AddMonoidHom` between their coefficients. -/
def mapDMatrix [∀ i j, AddMonoid (α i j)] {β : m → n → Type w} [∀ i j, AddMonoid (β i j)]
    (f : ∀ ⦃i j⦄, α i j →+ β i j) : DMatrix m n α →+ DMatrix m n β
    where
  toFun M := M.map fun i j => @f i j
  map_zero' := by simp
  map_add' := DMatrix.map_add f

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

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

Разделы

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

Аффилиация

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