Theorems · Theorem · linear algebra

Matrix.map_mul

∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {β : Type w} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : Fintype n] {L : Matrix m n α} {M : Matrix n o α} [inst_2 : NonUnitalNonAssocSemiring β] {F : Type u_10}
  [inst_3 : FunLike F α β] [NonUnitalRingHomClass F α β] {f : F}, (L * M).map ⇑f = L.map ⇑f * M.map ⇑f

Defined in

Mathlib.Data.Matrix.Mul

Cited by

9 results in Mathlib

Foundations

Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NonUnitalNonAssocSemiringFintypeNonUnitalNonAssocSemiringFunLikeNonUnitalRingHomClass