mapDMatrix_apply

Mathlib.Data.Matrix.DMatrix

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

Lean4

@[simp]
theorem mapDMatrix_apply [∀ i j, AddMonoid (α i j)] {β : m → n → Type w} [∀ i j, AddMonoid (β i j)]
    (f : ∀ ⦃i j⦄, α i j →+ β i j) (M : DMatrix m n α) : AddMonoidHom.mapDMatrix f M = M.map fun i j => @f i j :=
  rfl

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

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

Разделы

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

Аффилиация

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