proposition: Lemma form_eq0C u v : ('[u, v] == 0) = ('[v, u] == 0).
proof: Proof. by rewrite formC mulf_eq0 signr_eq0 /= fmorph_eq0. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix mxalgebra vector falgebra ssrnum algC algnum) mathcomp(fieldext) mathcomp(vector)