Theorems · Theorem · linear algebra

AddMonoidHom.entryAddMonoidHom_comp_mapMatrix

∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} [inst : AddZeroClass α] [inst_1 : AddZeroClass β]
  (f : α →+ β) (i : m) (j : n),
  (Matrix.entryAddMonoidHom β i j).comp f.mapMatrix = f.comp (Matrix.entryAddMonoidHom α i j)

Defined in: Mathlib.Data.Matrix.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 18 from the axioms · uses propext, Quot.sound
Assumes: AddZeroClass AddZeroClass

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Matrixstatement · cited by 4,303
AddMonoidHomstatement and proof · cited by 3,230
AddZeroClassstatement and proof · cited by 1,237
AddMonoidHom.compstatement · cited by 339
AddMonoidHom.mapMatrixstatement · cited by 9
Matrix.entryAddMonoidHomstatement · cited by 6

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.