proposition: Lemma matrix_sum_delta : forall A, A === \big[addmx/null_mx]_(i < m) \big[addmx/null_mx]_(j < n) (A i j *m: delta_mx i j).
proof: Proof. move=> A i j. setoid_rewrite summxE. setoid_rewrite summxE. setoid_rewrite (bigD1 (j:=i))=>//=. setoid_rewrite (big1 (P:=fun i0 => i0 != i))=>[|i0 Hi0]. setoid_rewrite (bigD1 (j:=j))=>//=. setoid_rewrite (big1 (P:=fun i0 => i0 != j))=>[|i0 Hi0]. by rewrite/delta_mx/scalemx !eq_refl/=; ring. rewrite/delta_mx/scalemx !eq_refl/= eq_sym; move:Hi0. by case/negbRL=>->/=; ring. apply (big1 (P:=fun _ => true) (F:=fun k => (A i0 k *m: delta_mx i0 k) i j))=>i1 _. rewrite/delta_mx/scalemx eq_sym/=; move:Hi0. by case/negbRL=>->/=; ring. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms