Theorems · Theorem · linear algebra

Matrix.isHermitian_mul_mul_conjTranspose

∀ {α : 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 n m α), A.IsHermitian → (B * A * B.conjTranspose).IsHermitian

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

Defined in

Mathlib.LinearAlgebra.Matrix.Hermitian

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonUnitalSemiringStarRingFintype