`BookProof.ChapterWeakValue.weakValue_one` (i f : Fin n → ℂ) (h : ip f i ≠ 0) : weakValue i f (1 : Matrix (Fin n) (Fin n) ℂ) = 1

Initializing...

`BookProof.ChapterWeakValue.weakValue_one` (i f : Fin n → ℂ) (h : ip f i ≠ 0) : weakValue i f (1 : Matrix (Fin n) (Fin n) ℂ) = 1 · Prove2Me