{R : Ring@{i}} {n : nat} (v : Vector R n) : matrix_transpose (matrix_diag v) = matrix_diag v. Proof. snrapply path_matrix. intros i j Hi Hj. rewrite 3 entry_Build_Matrix. rewrite kronecker_delta_symm. unfold kronecker_delta. destruct (dec (i = j)) as [p|np]. 1: f_ap; symmetry; by apply path_entry_vector. by rewrite !rng_mult_zero_l. 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.