Theorems · Theorem · linear algebra

Matrix.trace_conjTranspose_mul_self_eq_zero_iff

∀ {m : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : Fintype m] {R : Type u_5} [inst_2 : PartialOrder R]
  [inst_3 : NonUnitalRing R] [inst_4 : StarRing R] [StarOrderedRing R] [NoZeroDivisors R] {A : Matrix m n R},
  (A.conjTranspose * A).trace = 0 ↔ A = 0

Defined in

Mathlib.LinearAlgebra.Matrix.PosDef

Cited by

1 results in Mathlib

Foundations

Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeFintypePartialOrderNonUnitalRingStarRingStarOrderedRingNoZeroDivisors