Theorems · Theorem · linear algebra

Matrix.entryAddMonoidHom_eq_comp

∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} [inst : AddZeroClass α] {i : m} {j : n},
  Matrix.entryAddMonoidHom α i j =
    ((Pi.evalAddMonoidHom (fun x => α) j).comp (Pi.evalAddMonoidHom (fun i => n → α) i)).comp ↑Matrix.ofAddEquiv.symm

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites10

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

Matrixstatement · cited by 4,303
AddMonoidHomstatement · cited by 3,230
AddZeroClassstatement and proof · cited by 1,237
AddEquivstatement · cited by 1,087
AddEquiv.symmstatement · cited by 530
AddMonoidHom.compstatement · cited by 339
AddMonoidHomClass.toAddMonoidHomstatement · cited by 232
Pi.evalAddMonoidHomstatement · cited by 19
Matrix.entryAddMonoidHomstatement and proof · cited by 6
Matrix.ofAddEquivstatement · cited by 4

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.