`BookProof.ChapterWeakValue.weakValue_diag_isReal` (i : Fin n → ℂ) (A : Matrix (Fin n) (Fin n) ℂ) (hA : Aᴴ = A) (hi : ip i i = 1) : starRingEnd ℂ (weakValue i i A) = weakValue i i

Initializing...

`BookProof.ChapterWeakValue.weakValue_diag_isReal` (i : Fin n → ℂ) (A : Matrix (Fin n) (Fin n) ℂ) (hA : Aᴴ = A) (hi : ip i i = 1) : starRingEnd ℂ (weakValue i i A) = weakValue i i · Prove2Me