proposition: Lemma formC u v : '[u, v] = (-1) ^+ eps * theta '[v, u].
proof: Proof. rewrite /form [M in LHS](sesquiP _) // -mulmxA !mxE rmorph_sum mulr_sumr. apply: eq_bigr => /= i _; rewrite !(mxE, mulr_sumr, mulr_suml, rmorph_sum). apply: eq_bigr => /= j _; rewrite !mxE !rmorphM mulrCA -!mulrA. by congr (_ * _); rewrite mulrA mulrC /= thetaK. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix mxalgebra vector falgebra ssrnum algC algnum) mathcomp(fieldext) mathcomp(vector)