`BookProof.ChapterWeakValue.ip_smul_right` (c : ℂ) (f v : Fin n → ℂ) : ip f (c • v) = c * ip f v

Initializing...

`BookProof.ChapterWeakValue.ip_smul_right` (c : ℂ) (f v : Fin n → ℂ) : ip f (c • v) = c * ip f v · Prove2Me