proposition: Lemma cofactor_tr : forall n (A : 'M_n) i j, cofactor A^T i j === cofactor A j i.
proof: Proof. move=> n A i j; rewrite /cofactor addnC. apply rmul_morph; first by reflexivity. rewrite <- det_trmx; apply determinant_morph. by apply trmx_inj=>i' j'; apply trmxK. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms