Commit 2024-02-09 19:37 de7d014c

View on Github →

feat: Matrix.fromRows and Matrix.fromColumns multiplied by vectors (#10379) Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.E2.9C.94.20sumType_zeroFun_dotProduct

Estimated changes

Modified Mathlib/Data/Matrix/ColumnRowPartitioned.lean

added theorem Matrix.fromColumns_mulVec_sum_elim

added theorem Matrix.fromRows_mulVec

added theorem Matrix.sum_elim_vecMul_fromRows

modified theorem Matrix.toColumns₁_fromColumns

modified theorem Matrix.toColumns₂_fromColumns

added theorem Matrix.vecMul_fromColumns