proposition: Lemma Cayley_Hamilton : forall (a : CR) (X : matrix CR n 1), A *m X === a%:M *m X -> (char_poly ! a)%:M *m X === '0m.
proof: Proof. move=> a X Heq. rewrite char_poly_apply. rewrite <- mulmx_adjl. rewrite <- (mulmx0 (\adj (a%:M -m A))). rewrite <- mulmxA. apply mulmx_morph; first by reflexivity. rewrite -> mulmx_addl. Existing Instance addmx_morph. rewrite <- Heq=> i j {Heq}. rewrite /addmx /oppmx /mulmx /null_mx. have Heq : forall k, xpredT k -> [--](A i k)[*]X k j [=] [--](A i k[*]X k j) by move=> k _; ring. setoid_rewrite (eq_bigr _ Heq)=> {Heq}. setoid_rewrite <- (big_morph (op1:=csg_op) (idx1:=Zero) (phi:=fun x => [--]x))=> /=[|x y| |]; [by ring|by ring|by ring|]. move=> x x' eqx y y' eqy. by rewrite eqx eqy; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun paths perm CPoly_Degree Setoid Morphisms Ring CRingClass CPoly_Euclid bigopsClass matrixClass