Theorems · Definition · linear algebra

Matrix.diagonal

{n : Type u_3} → {α : Type v} → [DecidableEq n] → [Zero α] → (n → α) → Matrix n n α

diagonal d is the square matrix such that (diagonal d) i i = d i and (diagonal d) i j = 0 if i ≠ j. Note that bundled versions exist as: * Matrix.diagonalAddMonoidHom * Matrix.diagonalLinearMap * Matrix.diagonalRingHom * Matrix.diagonalAlgHom

Defined in

Mathlib.Data.Matrix.Diagonal

Cited by

314 results in Mathlib

Foundations

Depth 14 from the axioms, rests on 70 definitions · uses Quot.sound

Assumes

DecidableEqZero