proposition: Lemma Hilbert's_theorem_90 K E x a : generator 'Gal(E / K) x -> a \in E -> reflect (exists2 b, b \in E /\ b != 0 & a = b / x b) (galNorm K E a == 1).
proof: Proof. move/(_ =P <[x]>)=> DgalE Ea. have galEx: x \in 'Gal(E / K) by rewrite DgalE cycle_id. apply: (iffP eqP) => [normEa1 | [b [Eb nzb] ->]]; last first. by rewrite galNormM galNormV galNorm_gal // mulfV // galNorm_eq0. have [x1 | ntx] := eqVneq x 1%g. exists 1; first by rewrite mem1v oner_neq0. by rewrite -{1}normEa1 /galNorm DgalE x1 cycle1 big_set1 !gal_id divr1. pose c_ y := \prod_(i < invm (injm_Zpm x) y) (x ^+ i)%g a. have nz_c1: c_ 1%g != 0 by rewrite /c_ morph1 big_ord0 oner_neq0. have [d] := @gal_independent_contra _ [in 'Gal(E / K)] _ _ (group1 _) nz_c1. set b := \sum_(y in _) _ => Ed nz_b; exists b. split=> //; apply: rpred_sum => y galEy. by apply: rpredM; first apply: rpred_prod => i _; apply: memv_gal. apply: canRL (mulfK _) _; first by rewrite fmorph_eq0. rewrite rmorph_sum mulr_sumr [b](reindex_acts 'R _ galEx) ?astabsR //=. apply: eq_bigr => y galEy; rewrite galM // rmorphM mulrA; congr (_ * _). have /morphimP[/= i _ _ ->] /=: y \in Zpm @* Zp #[x] by rewrite im_Zpm -DgalE. have <-: Zpm (i + 1) = (Zpm i * x)%g by rewrite morphM ?mem_Zp ?order_gt1. rewrite /c_ !invmE ?mem_Zp ?order_gt1 //= addn1; set n := _.+2. transitivity (\prod_(j < i.+1) (x ^+ j)%g a). rewrite big_ord_recl gal_id rmorph_prod; congr (_ * _). by apply: eq_bigr => j _; rewrite expgSr galM ?lfunE. have [/modn_small->//||->] := ltngtP i.+1 n; first by rewrite ltnNge ltn_ord. rewrite modnn big_ord0; apply: etrans normEa1; rewrite /galNorm DgalE -im_Zpm. rewrite morphimEdom big_imset /=; last exact/injmP/injm_Zpm. by apply: eq_bigl => j /=; rewrite mem_Zp ?order_gt1. 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)