proposition: Lemma dim_aimg (F : fieldType) (L L' : fieldExtType F) (iota : 'AHom(L, L')) (E : {subfield L}) : \dim (iota @: E) = \dim E.
proof: Proof. suff /size_basis -> : basis_of (iota @: E) (map iota (vbasis E)) by []. by rewrite limg_basis_of// ?vbasisP// ?(eqP (AHom_lker0 _)) capv0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)