Theorems · Theorem · linear algebra

Matrix.conjTranspose_eq_transpose_of_trivial

∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Star α] [TrivialStar α] (A : Matrix m n α),
  A.conjTranspose = A.transpose

When star x = x on the coefficients (such as the real numbers) conjTranspose and transpose are the same operation.

Defined in

Mathlib.LinearAlgebra.Matrix.ConjTranspose

Cited by

2 results in Mathlib

Foundations

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

Assumes

StarTrivialStar