Theorems · Theorem · linear algebra

Matrix.PosSemidef.conjTranspose_mul_mul_same

∀ {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] [Finite m] {A : Matrix n n R},
  A.PosSemidef → ∀ (B : Matrix n m R), (B.conjTranspose * A * B).PosSemidef

Defined in

Mathlib.LinearAlgebra.Matrix.PosDef

Cited by

3 results in Mathlib

Foundations

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

Assumes

RingPartialOrderStarRingFintypeFinite