{R : Ring} {n : nat} (v w : Vector R n) : matrix_mult (matrix_diag v) (matrix_diag w) = matrix_diag (vector_map2 (.*.) v w). Proof. snrapply path_matrix. intros i j Hi Hj. rewrite 2 entry_Build_Matrix. lhs snrapply path_ab_sum. { intros k Hk. rewrite 2 entry_Build_Matrix. rewrite rng_mult_assoc. rewrite <- (rng_mult_assoc (kronecker_delta _ _)). rewrite kronecker_delta_comm. rewrite <- 2 rng_mult_assoc. reflexivity. } rewrite (rng_sum_kronecker_delta_l _ _ Hi). by rewrite entry_Build_Vector. Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Basics.Decidable. Require Import Types.Sigma. Require Import Spaces.List.Core Spaces.List.Theory Spaces.List.Paths. Require Import Algebra.Rings.Ring Algebra.Rings.Module Algebra.Rings.CRing Require Import abstract_algebra. Require Import WildCat.Core WildCat.Paths. Require Import Modalities.ReflectiveSubuniverse.