Theorems · Definition · linear algebra

Matrix.scalar

{α : Type u_11} →
  [inst : Semiring α] → (n : Type u) → [inst_1 : DecidableEq n] → [inst_2 : Fintype n] → α →+* Matrix n n α

The ring homomorphism α →+* Matrix n n α sending a to the diagonal matrix with a on the diagonal.

Defined in

Mathlib.Data.Matrix.Basic

Cited by

62 results in Mathlib

Foundations

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

Assumes

SemiringDecidableEqFintype