fact: Fixpoint gen_term t := match t with | 'X_k => row_var _ d k | x%:T => mx_term (val (x : FA)) | n1%:R => mx_term (val (n1%:R : FA))%R | t1 + t2 => \row_i (gen_term t1 0%R i + gen_term t2 0%R i) | - t1 => \row_i (- gen_term t1 0%R i) | t1 *+ n1 => mulmx_term (mx_term n1%:R%:M)%R (gen_term t1) | t1 * t2 => mulT (gen_term t1) (gen_term t2) | t1^-1 => gen_term t1 | t1 ^+ n1 => iter n1 (mulT (gen_term t1)) (mx_term (val (1%R : FA))) end%T.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv finset fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup matrix mxalgebra) mathcomp(mxpoly)