`BookProof.ChapterNumericalRangeCrouzeix.re_inner_sub_smul_nonneg` {A : E →L[ℂ] E} (h : NumRadiusLE A 1) {z : ℂ} (hz : ‖z‖ ≤ 1) (x : E) : 0 ≤ (⟪x, x

Initializing...

`BookProof.ChapterNumericalRangeCrouzeix.re_inner_sub_smul_nonneg` {A : E →L[ℂ] E} (h : NumRadiusLE A 1) {z : ℂ} (hz : ‖z‖ ≤ 1) (x : E) : 0 ≤ (⟪x, x - z • A x⟫_ℂ).re · Prove2Me