Theorems · Theorem · linear algebra

Matrix.conjTranspose_single

∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : DecidableEq m] [inst_2 : AddMonoid α]
  [inst_3 : StarAddMonoid α] (i : m) (j : n) (a : α), (Matrix.single i j a).conjTranspose = Matrix.single j i (star a)

Defined in

Mathlib.LinearAlgebra.Matrix.ConjTranspose

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqDecidableEqAddMonoidStarAddMonoid