Theorems · Definition · linear algebra

Matrix.entryAddMonoidHom

{m : Type u_2} → {n : Type u_3} → (α : Type u_11) → [inst : AddZeroClass α] → m → n → Matrix m n α →+ α

Extracting entries from a matrix as an additive monoid homomorphism. Note this cannot be upgraded to a ring homomorphism, as it does not respect multiplication.

Defined in

Mathlib.Data.Matrix.Basic

Cited by

6 results in Mathlib

Foundations

Depth 11 from the axioms · uses Quot.sound

Assumes

AddZeroClass