proposition: Lemma algR_normrMn x n : algR_norm (x *+ n) = algR_norm x *+ n.
proof: Proof. by apply/val_inj; rewrite /= !rmorphMn/= normrMn. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various)