Theorems · Theorem · linear algebra

Matrix.isHermitian_gram

∀ {E : Type u_1} {n : Type u_2} (𝕜 : Type u_4) [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] (v : n → E), (Matrix.gram 𝕜 v).IsHermitian

A Gram matrix is Hermitian.

Defined in: Mathlib.Analysis.InnerProductSpace.GramMatrix
Cited by: 3 results in Mathlib
Foundations: Depth 47 from the axioms · uses propext, Quot.sound
Assumes: RCLike SeminormedAddCommGroup InnerProductSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

InnerProductSpacestatement and proof · cited by 3,523
RCLikestatement and proof · cited by 2,829
SeminormedAddCommGroupstatement and proof · cited by 2,671
Matrix.extproof · cited by 540
Matrix.IsHermitianstatement · cited by 126
inner_conj_symmproof · cited by 48
Matrix.gramstatement · cited by 17

Cited by3

Results whose statement or proof uses this declaration.

Matrix.posSemidef_gramproof · cited by 4
Matrix.posDef_gram_of_linearIndependentproof · cited by 1
Matrix.posSemidef_opNorm_smul_gram_sub_gramproof · cited by 0