Theorems · Theorem · linear algebra

Matrix.isHermitian_conjTranspose_mul_mul

∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} [inst : NonUnitalSemiring α] [inst_1 : StarRing α] [inst_2 : Fintype m]
  {A : Matrix m m α} (B : Matrix m n α), A.IsHermitian → (B.conjTranspose * A * B).IsHermitian

Note this is more general than IsSelfAdjoint.conjugate' as B can be rectangular.

Defined in

Mathlib.LinearAlgebra.Matrix.Hermitian

Cited by

3 results in Mathlib

Foundations

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

Assumes

NonUnitalSemiringStarRingFintype