Commit 2026-05-01 15:28 eaccec82

feat(Data/Matrix/Mul): add diagonal and transpose lemmas for vector operations (#34851) This adds three lemmas for matrix-vector operations that serve as foundational support for future ML formalization:

• vecMul_diagonal_dotProduct: weighted inner product x ᵥ* diagonal d ⬝ᵥ y = ∑ i, d i * x i * y i
• mul_diagonal_mulVec: column-weighted sum (A * diagonal d) *ᵥ x = ∑ i, (d i * x i) • A.col i These are basic linear algebra identities involving diagonal matrices and vector operations that appear frequently in machine learning contexts (weighted inner products, attention mechanisms, feature scaling, diagonal preconditioning).