Theorems · Definition · linear algebra

PEquiv.toMatrix

{m : Type u_3} → {n : Type u_4} → {α : Type u_5} → [DecidableEq n] → [Zero α] → [One α] → (m ≃. n) → Matrix m n α

toMatrix returns a matrix containing ones and zeros. f.toMatrix i j is 1 if f i = some j and 0 otherwise

Defined in

Mathlib.Data.Matrix.PEquiv

Cited by

25 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext, Quot.sound

Assumes

DecidableEqZeroOne