proposition: Lemma similar_det m n (A : 'M[R]_m) (B : 'M[R]_n) : similar A B -> \det A = \det B.
proof: Proof. case=> [Hmn]; move: Hmn A B=> -> A B [P HP HAB]. apply: (@mulrI _ (\det P)); first by rewrite -unitmxE. by rewrite -det_mulmx mulrC -det_mulmx HAB conform_mx_id. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype fintype finfun ssrnat seq) mathcomp(choice ssralg poly polydiv mxpoly matrix bigop) mathcomp(mxalgebra perm fingroup tuple) mxstructure dvdring