Theorems · Theorem · linear algebra

Matrix.map_single

∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : Zero α] (i : m)
  (j : n) (a : α) {β : Type u_10} [inst_3 : Zero β] {F : Type u_11} [inst_4 : FunLike F α β] [ZeroHomClass F α β]
  (f : F), (Matrix.single i j a).map ⇑f = Matrix.single i j (f a)

Defined in

Mathlib.Data.Matrix.Basis

Cited by

2 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Quot.sound

Assumes

DecidableEqDecidableEqZeroZeroFunLikeZeroHomClass