Theorem Matrix.dot_mulVec_eq_sum_sum

Modification history

2026-06-12 12:02
Mathlib/Data/Matrix/Mul.lean
feat: prove elementary spectral bound for Z-matrices (#40372) …
Added Matrix.dot_mulVec_eq_sum_sumView on Github →