`BookProof.ChapterNumericalRangeCrouzeix.inner_sub_const_smul` (A : E →L[ℂ] E) (c : ℂ) (x : E) : (⟪ x, (A - c • (1 : E →L[ℂ] E)) x ⟫_ℂ) = ⟪ x, A x ⟫_ℂ

Initializing...

`BookProof.ChapterNumericalRangeCrouzeix.inner_sub_const_smul` (A : E →L[ℂ] E) (c : ℂ) (x : E) : (⟪ x, (A - c • (1 : E →L[ℂ] E)) x ⟫_ℂ) = ⟪ x, A x ⟫_ℂ - c * (‖x‖ ^ 2 : ℝ) · Prove2Me