proposition: Lemma aut_mem_eqP E (x y : coset_of (kAEndf E)) f g : f \in x -> g \in y -> reflect {in E, f =1 g} (x == y).
proof: Proof. move=> x_f y_g; rewrite -(coset_mem x_f) -(coset_mem y_g). have [Nf Ng] := (subsetP (coset_norm x) f x_f, subsetP (coset_norm y) g y_g). rewrite (sameP eqP (rcoset_kercosetP Nf Ng)) mem_rcoset inE kAutfE. apply: (iffP kAHomP) => idEfg u Eu. by rewrite -(mulgKV g f) lfunE /= idEfg. by rewrite (@lfunE _ _ L) /= idEfg // lker0_lfunK ?AEnd_lker0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg poly) mathcomp(polydiv finset fingroup morphism quotient perm) mathcomp(action zmodp cyclic matrix mxalgebra vector) mathcomp(falgebra fieldext separable)