Theorems · Theorem · linear algebra

Matrix.PosDef.mul_conjTranspose_self

∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : Fintype n] [inst_4 : Fintype m] [StarOrderedRing R] [NoZeroDivisors R] (A : Matrix m n R),
  (Function.Injective fun v => Matrix.vecMul v A) → (A * A.conjTranspose).PosDef

Defined in

Mathlib.LinearAlgebra.Matrix.PosDef

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingPartialOrderStarRingFintypeFintypeStarOrderedRingNoZeroDivisors