proposition: Lemma char_poly_apply : forall a : CR, char_poly ! a === \det (a%:M -m A).
proof: Proof. rewrite /char_poly /determinant=> a. rewrite apply_bigsum. apply eq_bigr=> s _. rewrite -> mult_apply. apply csbf_wd. case: (odd_perm s)=> /=; last by apply one_apply. rewrite /Equivalence.equiv. rewrite (mult_apply CR). apply csbf_wd; last by apply one_apply. rewrite -> inv_apply. rewrite -> one_apply. by reflexivity. rewrite apply_big_prod. apply eq_bigr=> i _. rewrite /scalar_mx /addmx /oppmx /matrixC. rewrite -> plus_apply. rewrite -> inv_apply. rewrite -> c_apply. apply csbf_wd; last by reflexivity. case: (i == s i); first by apply x_apply. by apply poly_eq_zero; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun paths perm CPoly_Degree Setoid Morphisms Ring CRingClass CPoly_Euclid bigopsClass matrixClass