proposition: Lemma gal_adjoin_eq K a x y : x \in 'Gal(<<K; a>> / K) -> y \in 'Gal(<<K; a>> / K) -> (x == y) = (x a == y a).
proof: Proof. move=> galKa_x galKa_y; apply/idP/eqP=> [/eqP-> // | eq_xy_a]. apply/gal_eqP => _ /Fadjoin_polyP[p Kp ->]. by rewrite -!horner_map !(fixedPoly_gal (subv_adjoin K a)) //= eq_xy_a. 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)