Theorems · Theorem · linear algebra

Matrix.transpose_single

∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : Zero α] (i : m)
  (j : n) (a : α), (Matrix.single i j a).transpose = Matrix.single j i a

Defined in

Mathlib.Data.Matrix.Basis

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEqDecidableEqZero