Theorems · Theorem · linear algebra

LinearMap.isHermitian_toMatrix_iff

∀ {n : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : RCLike 𝕜]
  [inst_3 : NormedAddCommGroup E] [inst_4 : InnerProductSpace 𝕜 E] {f : E →ₗ[𝕜] E} (b : OrthonormalBasis n 𝕜 E),
  ((LinearMap.toMatrix b.toBasis b.toBasis) f).IsHermitian ↔ f.IsSymmetric

A linear map is symmetric iff the corresponding matrix with an orthonormal basis is Hermitian.

Defined in

Mathlib.Analysis.Matrix.Hermitian

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqRCLikeNormedAddCommGroupInnerProductSpace