Initial commit

1 files changed, 835 insertions, 0 deletions

diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v
new file mode 100644
index 0000000..cff3197
--- /dev/null
+++ b/mathcomp/field/algnum.v
@@ -0,0 +1,835 @@
+(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path div choice.
+Require Import fintype tuple finfun bigop prime ssralg finalg zmodp poly.
+Require Import ssrnum ssrint rat polydiv intdiv algC matrix mxalgebra mxpoly.
+Require Import vector falgebra fieldext separable galois cyclotomic.
+
+(******************************************************************************)
+(* This file provides a few basic results and constructions in algebraic      *)
+(* number theory, that are used in the character theory library. Most of      *)
+(* these could be generalized to a more abstract setting. Note that the type  *)
+(* of abstract number fields is simply extFieldType rat. We define here:      *)
+(*  x \in Crat_span X <=> x is a Q-linear combination of elements of          *)
+(*                        X : seq algC.                                       *)
+(*  x \in Cint_span X <=> x is a Z-linear combination of elements of          *)
+(*                        X : seq algC.                                       *)
+(*         x \in Aint <=> x : algC is an algebraic integer, i.e., the (monic) *)
+(*                        polynomial of x over Q has integer coeficients.     *)
+(*         (e %| a)%A <=> e divides a with respect to algebraic integers,     *)
+(*        (e %| a)%Ax     i.e., a is in the algebraic integer ideal generated *)
+(*                        by e. This is is notation for a \in dvdA e, where   *)
+(*                        dvdv is the (collective) predicate for the Aint     *)
+(*                        ideal generated by e. As in the (e %| a)%C notation *)
+(*                        e and a can be coerced to algC from nat or int.     *)
+(*                        The (e %| a)%Ax display form is a workaround for    *)
+(*                        design limitations of the Coq Notation facilities.  *)
+(* (a == b %[mod e])%A, (a != b %[mod e])%A <=>                               *)
+(*                       a is equal (resp. not equal) to b mod e, i.e., a and *)
+(*                       b belong to the same e * Aint class. We do not       *)
+(*                       force a, b and e to be algebraic integers.           *)
+(*            #[x]%C == the multiplicative order of x, i.e., the n such that  *)
+(*                      x is an nth primitive root of unity, or 0 if x is not *)
+(*                      a root of unity.                                      *)
+(* In addition several lemmas prove the (constructive) existence of number    *)
+(* fields and of automorphisms of algC.                                       *)
+(******************************************************************************)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Import GRing.Theory Num.Theory.
+Local Open Scope ring_scope.
+
+Local Notation ZtoQ := (intr : int -> rat).
+Local Notation ZtoC := (intr : int -> algC).
+Local Notation QtoC := (ratr : rat -> algC).
+
+Local Notation intrp := (map_poly intr).
+Local Notation pZtoQ := (map_poly ZtoQ).
+Local Notation pZtoC := (map_poly ZtoC).
+Local Notation pQtoC := (map_poly ratr).
+
+Local Hint Resolve (@intr_inj _ : injective ZtoC).
+Local Notation QtoCm := [rmorphism of QtoC].
+
+(* Number fields and rational spans. *)
+Lemma algC_PET (s : seq algC) :
+  {z | exists a : nat ^ size s, z = \sum_(i < size s) s`_i *+ a i
+     & exists ps, s = [seq (pQtoC p).[z] | p <- ps]}.
+Proof.
+elim: s => [|x s [z /sig_eqW[a Dz] /sig_eqW[ps Ds]]].
+  by exists 0; [exists [ffun _ => 2]; rewrite big_ord0 | exists nil].
+have r_exists (y : algC): {r | r != 0 & root (pQtoC r) y}.
+  have [r [_ mon_r] dv_r] := minCpolyP y.
+  by exists r; rewrite ?monic_neq0 ?dv_r.
+suffices /sig_eqW[[n [|px [|pz []]]]// [Dpx Dpz]]:
+  exists np, let zn := x *+ np.1 + z in
+    [:: x; z] = [seq (pQtoC p).[zn] | p <- np.2].
+- exists (x *+ n + z).
+    exists [ffun i => oapp a n (unlift ord0 i)].
+    rewrite /= big_ord_recl ffunE unlift_none Dz; congr (_ + _).
+    by apply: eq_bigr => i _; rewrite ffunE liftK.
+  exists (px :: [seq p \Po pz | p <- ps]); rewrite /= -Dpx; congr (_ :: _).
+  rewrite -map_comp Ds; apply: eq_map => p /=.
+  by rewrite map_comp_poly horner_comp -Dpz.
+have [rx nz_rx rx0] := r_exists x.
+have [rz nz_rz rz0] := r_exists (- z).
+have char0_Q: [char rat] =i pred0 by exact: char_num.
+have [n [[pz Dpz] [px Dpx]]] := char0_PET nz_rz rz0 nz_rx rx0 char0_Q.
+by exists (n, [:: px; - pz]); rewrite /= !raddfN hornerN -[z]opprK Dpz Dpx.
+Qed.
+
+Canonical subfx_unitAlgType (F L : fieldType) iota (z : L) p :=
+  Eval hnf in [unitAlgType F of subFExtend iota z p].
+
+Lemma num_field_exists (s : seq algC) :
+  {Qs : fieldExtType rat & {QsC : {rmorphism Qs -> algC}
+   & {s1 : seq Qs | map QsC s1 = s & <<1 & s1>>%VS = fullv}}}.
+Proof.
+have [z /sig_eqW[a Dz] /sig_eqW[ps Ds]] := algC_PET s.
+suffices [Qs [QsC [z1 z1C z1gen]]]:
+  {Qs : fieldExtType rat & {QsC : {rmorphism Qs -> algC} &
+     {z1 : Qs | QsC z1 = z & forall xx, exists p, fieldExt_horner z1 p = xx}}}.
+- set inQs := fieldExt_horner z1 in z1gen *; pose s1 := map inQs ps.
+  have inQsK p: QsC (inQs p) = (pQtoC p).[z].
+    rewrite /= -horner_map z1C -map_poly_comp; congr _.[z].
+    apply: eq_map_poly => b /=; apply: canRL (mulfK _) _.
+      by rewrite intr_eq0 denq_eq0.
+    rewrite /= mulrzr -rmorphMz scalerMzl -{1}[b]divq_num_den -mulrzr.
+    by rewrite divfK ?intr_eq0 ?denq_eq0 // scaler_int rmorph_int.
+  exists Qs, QsC, s1; first by rewrite -map_comp Ds (eq_map inQsK).
+  have sz_ps: size ps = size s by rewrite Ds size_map.
+  apply/vspaceP=> x; rewrite memvf; have [p {x}<-] := z1gen x.
+  elim/poly_ind: p => [|p b ApQs]; first by rewrite /inQs rmorph0 mem0v.
+  rewrite /inQs rmorphD rmorphM /= fieldExt_hornerX fieldExt_hornerC -/inQs /=.
+  suffices ->: z1 = \sum_(i < size s) s1`_i *+ a i.
+    rewrite memvD ?memvZ ?mem1v ?memvM ?memv_suml // => i _.
+    by rewrite rpredMn ?seqv_sub_adjoin ?mem_nth // size_map sz_ps.
+  apply: (fmorph_inj QsC); rewrite z1C Dz rmorph_sum; apply: eq_bigr => i _.
+  by rewrite rmorphMn {1}Ds !(nth_map 0) ?sz_ps //= inQsK.
+have [r [Dr /monic_neq0 nz_r] dv_r] := minCpolyP z.
+have rz0: root (pQtoC r) z by rewrite dv_r.
+have irr_r: irreducible_poly r.
+  by apply/(subfx_irreducibleP rz0 nz_r)=> q qz0 nzq; rewrite dvdp_leq // -dv_r.
+exists (SubFieldExtType rz0 irr_r), (subfx_inj_rmorphism QtoCm z r).
+exists (subfx_root _ z r) => [|x]; first exact: subfx_inj_root.
+by have{x} [p ->] := subfxEroot rz0 nz_r x; exists p.
+Qed.
+
+Definition in_Crat_span s x :=
+  exists a : rat ^ size s, x = \sum_i QtoC (a i) * s`_i.
+
+Fact Crat_span_subproof s x : decidable (in_Crat_span s x).
+Proof.
+have [Qxs [QxsC [[|x1 s1] // [<- <-] {x s} _]]] := num_field_exists (x :: s).
+have QxsC_Z a zz: QxsC (a *: zz) = QtoC a * QxsC zz.
+  rewrite mulrAC; apply: (canRL (mulfK _)); first by rewrite intr_eq0 denq_eq0.
+  by rewrite mulrzr mulrzl -!rmorphMz scalerMzl -mulrzr -numqE scaler_int.
+apply: decP (x1 \in <<in_tuple s1>>%VS) _; rewrite /in_Crat_span size_map.
+apply: (iffP idP) => [/coord_span-> | [a Dx]].
+  move: (coord _) => a; exists [ffun i => a i x1]; rewrite rmorph_sum.
+  by apply: eq_bigr => i _; rewrite ffunE (nth_map 0).
+have{Dx} ->: x1 = \sum_i a i *: s1`_i.
+  apply: (fmorph_inj QxsC); rewrite Dx rmorph_sum.
+  by apply: eq_bigr => i _; rewrite QxsC_Z (nth_map 0).
+by apply: memv_suml => i _; rewrite memvZ ?memv_span ?mem_nth.
+Qed.
+
+Definition Crat_span s : pred algC := Crat_span_subproof s.
+Lemma Crat_spanP s x : reflect (in_Crat_span s x) (x \in Crat_span s).
+Proof. exact: sumboolP. Qed.
+Fact Crat_span_key s : pred_key (Crat_span s). Proof. by []. Qed.
+Canonical Crat_span_keyed s := KeyedPred (Crat_span_key s).
+
+Lemma mem_Crat_span s : {subset s <= Crat_span s}.
+Proof.
+move=> _ /(nthP 0)[ix ltxs <-]; pose i0 := Ordinal ltxs.
+apply/Crat_spanP; exists [ffun i => (i == i0)%:R].
+rewrite (bigD1 i0) //= ffunE eqxx // rmorph1 mul1r.
+by rewrite big1 ?addr0 // => i; rewrite ffunE rmorph_nat mulr_natl => /negbTE->.
+Qed.
+
+Fact Crat_span_zmod_closed s : zmod_closed (Crat_span s).
+Proof.
+split=> [|_ _ /Crat_spanP[x ->] /Crat_spanP[y ->]].
+  apply/Crat_spanP; exists 0.
+  by apply/esym/big1=> i _; rewrite ffunE rmorph0 mul0r.
+apply/Crat_spanP; exists (x - y); rewrite -sumrB; apply: eq_bigr => i _.
+by rewrite -mulrBl -rmorphB !ffunE.
+Qed.
+Canonical Crat_span_opprPred s := OpprPred (Crat_span_zmod_closed s).
+Canonical Crat_span_addrPred s := AddrPred (Crat_span_zmod_closed s).
+Canonical Crat_span_zmodPred s := ZmodPred (Crat_span_zmod_closed s).
+
+Section MoreAlgCaut.
+
+Implicit Type rR : unitRingType.
+
+Lemma alg_num_field (Qz : fieldExtType rat) a : a%:A = ratr a :> Qz.
+Proof. by rewrite -in_algE fmorph_eq_rat. Qed.
+
+Lemma rmorphZ_num (Qz : fieldExtType rat) rR (f : {rmorphism Qz -> rR}) a x :
+  f (a *: x) = ratr a * f x.
+Proof. by rewrite -mulr_algl rmorphM alg_num_field fmorph_rat. Qed.
+
+Lemma fmorph_numZ (Qz1 Qz2 : fieldExtType rat) (f : {rmorphism Qz1 -> Qz2}) :
+  scalable f.
+Proof. by move=> a x; rewrite rmorphZ_num -alg_num_field mulr_algl. Qed.
+Definition NumLRmorphism Qz1 Qz2 f := AddLRMorphism (@fmorph_numZ Qz1 Qz2 f).
+
+End MoreAlgCaut.
+
+Section NumFieldProj.
+
+Variables (Qn : fieldExtType rat) (QnC : {rmorphism Qn -> algC}).
+
+Lemma Crat_spanZ b a : {in Crat_span b, forall x, ratr a * x \in Crat_span b}.
+Proof.
+move=> _ /Crat_spanP[a1 ->]; apply/Crat_spanP; exists [ffun i => a * a1 i].
+by rewrite mulr_sumr; apply: eq_bigr => i _; rewrite ffunE mulrA -rmorphM.
+Qed.
+
+Lemma Crat_spanM b : {in Crat & Crat_span b, forall a x, a * x \in Crat_span b}.
+Proof. by move=> _ x /CratP[a ->]; exact: Crat_spanZ. Qed.
+
+(* In principle CtoQn could be taken to be additive and Q-linear, but this    *)
+(* would require a limit construction.                                        *)
+Lemma num_field_proj : {CtoQn | CtoQn 0 = 0 & cancel QnC CtoQn}.
+Proof.
+pose b := vbasis {:Qn}.
+have Qn_bC (u : {x | x \in Crat_span (map QnC b)}): {y | QnC y = sval u}.
+  case: u => _ /= /Crat_spanP/sig_eqW[a ->].
+  exists (\sum_i a i *: b`_i); rewrite rmorph_sum; apply: eq_bigr => i _.
+  by rewrite rmorphZ_num (nth_map 0) // -(size_map QnC).
+pose CtoQn x := oapp (fun u => sval (Qn_bC u)) 0 (insub x).
+suffices QnCK: cancel QnC CtoQn by exists CtoQn; rewrite // -(rmorph0 QnC).
+move=> x; rewrite /CtoQn insubT => /= [|Qn_x]; last first.
+  by case: (Qn_bC _) => x1 /= /fmorph_inj.
+rewrite (coord_vbasis (memvf x)) rmorph_sum rpred_sum // => i _.
+rewrite rmorphZ_num Crat_spanZ ?mem_Crat_span // -/b.
+by rewrite -tnth_nth -tnth_map mem_tnth.
+Qed.
+
+Lemma restrict_aut_to_num_field (nu : {rmorphism algC -> algC}) :
+    (forall x, exists y, nu (QnC x) = QnC y) ->
+  {nu0 : {lrmorphism Qn -> Qn} | {morph QnC : x / nu0 x >-> nu x}}.
+Proof.
+move=> Qn_nu; pose nu0 x := sval (sig_eqW (Qn_nu x)).
+have QnC_nu0: {morph QnC : x / nu0 x >-> nu x}.
+  by rewrite /nu0 => x; case: (sig_eqW _).
+suffices nu0M: rmorphism nu0 by exists (NumLRmorphism (RMorphism nu0M)).
+do 2?split=> [x y|]; apply: (fmorph_inj QnC); rewrite ?QnC_nu0 ?rmorph1 //.
+  by rewrite ?(rmorphB, QnC_nu0).
+by rewrite ?(rmorphM, QnC_nu0).
+Qed.
+
+Lemma map_Qnum_poly (nu : {rmorphism algC -> algC}) p :
+  p \in polyOver 1%VS -> map_poly (nu \o QnC) p = (map_poly QnC p).
+Proof.
+move=> Qp; apply/polyP=> i; rewrite /= !coef_map /=.
+have /vlineP[a ->]: p`_i \in 1%VS by exact: polyOverP.
+by rewrite alg_num_field !fmorph_rat.
+Qed.
+
+End NumFieldProj.
+
+Lemma restrict_aut_to_normal_num_field (Qn : splittingFieldType rat)
+  (QnC : {rmorphism Qn -> algC})(nu : {rmorphism algC -> algC}) :
+    {nu0 : {lrmorphism Qn -> Qn} | {morph QnC : x / nu0 x >-> nu x}}.
+Proof.
+apply: restrict_aut_to_num_field => x.
+case: (splitting_field_normal 1%AS x) => rs /eqP Hrs.
+have: root (map_poly (nu \o QnC) (minPoly 1%AS x)) (nu (QnC x)).
+  by rewrite fmorph_root root_minPoly.
+rewrite map_Qnum_poly ?minPolyOver // Hrs.
+rewrite [map_poly _ _](_:_ = \prod_(y <- map QnC rs) ('X - y%:P)); last first.
+  rewrite big_map rmorph_prod; apply eq_bigr => i _.
+  by rewrite rmorphB /= map_polyX map_polyC.
+rewrite root_prod_XsubC.
+by case/mapP => y _ ?; exists y.
+Qed.
+
+(* Integral spans. *)
+
+Lemma dec_Cint_span (V : vectType algC) m (s : m.-tuple V) v :
+  decidable (inIntSpan s v).
+Proof.
+have s_s (i : 'I_m): s`_i \in <<s>>%VS by rewrite memv_span ?memt_nth.
+have s_Zs a: \sum_(i < m) s`_i *~ a i \in <<s>>%VS.
+  by rewrite memv_suml // => i _; rewrite -scaler_int memvZ.
+case s_v: (v \in <<s>>%VS); last by right=> [[a Dv]]; rewrite Dv s_Zs in s_v.
+pose IzT := {: 'I_m * 'I_(\dim <<s>>)}; pose Iz := 'I_#|IzT|.
+pose b := vbasis <<s>>.
+pose z_s := [seq coord b ij.2 (tnth s ij.1) | ij : IzT].
+pose rank2 j i: Iz := enum_rank (i, j); pose val21 (p : Iz) := (enum_val p).1.
+pose inQzs w := [forall j, Crat_span z_s (coord b j w)].
+have enum_pairK j: {in predT, cancel (rank2 j) val21}.
+  by move=> i; rewrite /val21 enum_rankK. 
+have Qz_Zs a: inQzs (\sum_(i < m) s`_i *~ a i).
+  apply/forallP=> j; apply/Crat_spanP; rewrite /in_Crat_span size_map -cardE.
+  exists [ffun ij => (a (val21 ij))%:Q *+ ((enum_val ij).2 == j)].
+  rewrite linear_sum {1}(reindex_onto _ _ (enum_pairK j)).
+  rewrite big_mkcond; apply: eq_bigr => ij _ /=; rewrite nth_image (tnth_nth 0).
+  rewrite (can2_eq (@enum_rankK _) (@enum_valK _)) ffunE -scaler_int /val21.
+  case Dij: (enum_val ij) => [i j1]; rewrite xpair_eqE eqxx /= eq_sym -mulrb.
+  by rewrite linearZ rmorphMn rmorph_int mulrnAl; case: eqP => // ->.
+case Qz_v: (inQzs v); last by right=> [[a Dv]]; rewrite Dv Qz_Zs in Qz_v.
+have [Qz [QzC [z1s Dz_s _]]] := num_field_exists z_s.
+have sz_z1s: size z1s = #|IzT| by rewrite -(size_map QzC) Dz_s size_map cardE.
+have xv j: {x | coord b j v = QzC x}.
+  apply: sig_eqW; have /Crat_spanP[x ->] := forallP Qz_v j.
+  exists (\sum_ij x ij *: z1s`_ij); rewrite rmorph_sum.
+  apply: eq_bigr => ij _; rewrite mulrAC.
+  apply: canLR (mulfK _) _; first by rewrite intr_eq0 denq_neq0.
+  rewrite mulrzr -rmorphMz scalerMzl -(mulrzr (x _)) -numqE scaler_int.
+  by rewrite rmorphMz mulrzl -(nth_map _ 0) ?Dz_s // -(size_map QzC) Dz_s.
+pose sz := [tuple [ffun j => z1s`_(rank2 j i)] | i < m].
+have [Zsv | Zs'v] := dec_Qint_span sz [ffun j => sval (xv j)].
+  left; have{Zsv} [a Dv] := Zsv; exists a.
+  transitivity (\sum_j \sum_(i < m) QzC ((sz`_i *~ a i) j) *: b`_j).
+    rewrite {1}(coord_vbasis s_v) -/b; apply: eq_bigr => j _.
+    rewrite -scaler_suml; congr (_ *: _).
+    have{Dv} /ffunP/(_ j) := Dv; rewrite sum_ffunE !ffunE -rmorph_sum => <-.
+    by case: (xv j).
+  rewrite exchange_big; apply: eq_bigr => i _.
+  rewrite (coord_vbasis (s_s i)) -/b mulrz_suml; apply: eq_bigr => j _.
+  rewrite scalerMzl ffunMzE rmorphMz; congr ((_ *~ _) *: _).
+  rewrite nth_mktuple ffunE -(nth_map _ 0) ?sz_z1s // Dz_s.
+  by rewrite nth_image enum_rankK /= (tnth_nth 0).
+right=> [[a Dv]]; case: Zs'v; exists a.
+apply/ffunP=> j; rewrite sum_ffunE !ffunE; apply: (fmorph_inj QzC).
+case: (xv j) => /= _ <-; rewrite Dv linear_sum rmorph_sum.
+apply: eq_bigr => i _; rewrite nth_mktuple raddfMz !ffunMzE rmorphMz ffunE.
+by rewrite -(nth_map _ 0 QzC) ?sz_z1s // Dz_s nth_image enum_rankK -tnth_nth.
+Qed.
+
+Definition Cint_span (s : seq algC) : pred algC :=
+  fun x => dec_Cint_span (in_tuple [seq \row_(i < 1) y | y <- s]) (\row_i x).
+Fact Cint_span_key s : pred_key (Cint_span s). Proof. by []. Qed.
+Canonical Cint_span_keyed s := KeyedPred (Cint_span_key s).
+
+Lemma Cint_spanP n (s : n.-tuple algC) x :
+  reflect (inIntSpan s x) (x \in Cint_span s).
+Proof.
+rewrite unfold_in; case: (dec_Cint_span _ _) => [Zs_x | Zs'x] /=.
+  left; have{Zs_x} [] := Zs_x; rewrite /= size_map size_tuple => a /rowP/(_ 0).
+  rewrite !mxE => ->; exists a; rewrite summxE; apply: eq_bigr => i _.
+  by rewrite -scaler_int (nth_map 0) ?size_tuple // !mxE mulrzl.
+right=> [[a Dx]]; have{Zs'x} [] := Zs'x.
+rewrite /inIntSpan /= size_map size_tuple; exists a.
+apply/rowP=> i0; rewrite !mxE summxE Dx; apply: eq_bigr => i _.
+by rewrite -scaler_int mxE mulrzl (nth_map 0) ?size_tuple // !mxE.
+Qed.
+
+Lemma mem_Cint_span s : {subset s <= Cint_span s}.
+Proof.
+move=> _ /(nthP 0)[ix ltxs <-]; apply/(Cint_spanP (in_tuple s)).
+exists [ffun i => i == Ordinal ltxs : int].
+rewrite (bigD1 (Ordinal ltxs)) //= ffunE eqxx.
+by rewrite big1 ?addr0 // => i; rewrite ffunE => /negbTE->.
+Qed.
+
+Lemma Cint_span_zmod_closed s : zmod_closed (Cint_span s).
+Proof.
+have sP := Cint_spanP (in_tuple s); split=> [|_ _ /sP[x ->] /sP[y ->]].
+  by apply/sP; exists 0; rewrite big1 // => i; rewrite ffunE.
+apply/sP; exists (x - y); rewrite -sumrB; apply: eq_bigr => i _.
+by rewrite !ffunE raddfB.
+Qed.
+Canonical Cint_span_opprPred s := OpprPred (Cint_span_zmod_closed s).
+Canonical Cint_span_addrPred s := AddrPred (Cint_span_zmod_closed s).
+Canonical Cint_span_zmodPred s := ZmodPred (Cint_span_zmod_closed s).
+
+(* Automorphism extensions. *)
+Lemma extend_algC_subfield_aut (Qs : fieldExtType rat)
+  (QsC : {rmorphism Qs -> algC}) (phi : {rmorphism Qs -> Qs}) :
+  {nu : {rmorphism algC -> algC} | {morph QsC : x / phi x >-> nu x}}.
+Proof.
+pose numF_inj (Qr : fieldExtType rat) := {rmorphism Qr -> algC}.
+pose subAut := {Qr : _ & numF_inj Qr * {lrmorphism Qr -> Qr}}%type.
+pose SubAut := existS _ _ (_, _) : subAut.
+pose Sdom (mu : subAut) := projS1 mu.
+pose Sinj (mu : subAut) : {rmorphism Sdom mu -> algC} := (projS2 mu).1.
+pose Saut (mu : subAut) : {rmorphism Sdom mu -> Sdom mu} := (projS2 mu).2.
+have SinjZ Qr (QrC : numF_inj Qr) a x: QrC (a *: x) = QtoC a * QrC x.
+  rewrite mulrAC; apply: canRL (mulfK _) _.
+    by rewrite intr_eq0 denq_neq0.
+  by rewrite mulrzr mulrzl -!rmorphMz scalerMzl -scaler_int -mulrzr -numqE.
+have Sinj_poly Qr (QrC : numF_inj Qr) p:
+  map_poly QrC (map_poly (in_alg Qr) p) = pQtoC p.
+- rewrite -map_poly_comp; apply: eq_map_poly => a.
+  by rewrite /= SinjZ rmorph1 mulr1.
+have ext1 mu0 x: {mu1 | exists y, x = Sinj mu1 y
+  & exists2 in01 : {lrmorphism _}, Sinj mu0 =1 Sinj mu1 \o in01
+  & {morph in01: y / Saut mu0 y >-> Saut mu1 y}}.
+- pose b0 := vbasis {:Sdom mu0}.
+  have [z _ /sig_eqW[[|px ps] // [Dx Ds]]] := algC_PET (x :: map (Sinj mu0) b0).
+  have [p [_ mon_p] /(_ p) pz0] := minCpolyP z; rewrite dvdpp in pz0.
+  have [r Dr] := closed_field_poly_normal (pQtoC p : {poly algC}).
+  rewrite lead_coef_map {mon_p}(monicP mon_p) rmorph1 scale1r in Dr.
+  have{pz0} rz: z \in r by rewrite -root_prod_XsubC -Dr.
+  have [Qr [QrC [rr Drr genQr]]] := num_field_exists r.
+  have{rz} [zz Dz]: {zz | QrC zz = z}.
+    by move: rz; rewrite -Drr => /mapP/sig2_eqW[zz]; exists zz.
+  have{ps Ds} [in01 Din01]: {in01 : {lrmorphism _} | Sinj mu0 =1 QrC \o in01}.
+    have in01P y: {yy | Sinj mu0 y = QrC yy}.
+      exists (\sum_i coord b0 i y *: (map_poly (in_alg Qr) ps`_i).[zz]).
+      rewrite {1}(coord_vbasis (memvf y)) !rmorph_sum; apply: eq_bigr => i _.
+      rewrite !SinjZ; congr (_ * _); rewrite -(nth_map _ 0) ?size_tuple // Ds.
+      rewrite -horner_map Dz Sinj_poly (nth_map 0) //.
+      by have:= congr1 size Ds; rewrite !size_map size_tuple => <-.
+    pose in01 y := sval (in01P y).
+    have Din01 y: Sinj mu0 y = QrC (in01 y) by rewrite /in01; case: (in01P y).
+    suffices in01M: lrmorphism in01 by exists (LRMorphism in01M).
+    pose rwM := (=^~ Din01, SinjZ, rmorph1, rmorphB, rmorphM).
+    by do 3?split; try move=> ? ?; apply: (fmorph_inj QrC); rewrite !rwM.
+  have {z zz Dz px Dx} Dx: exists xx, x = QrC xx.
+    exists (map_poly (in_alg Qr) px).[zz].
+    by rewrite -horner_map Dz Sinj_poly Dx.
+  pose lin01 := linfun in01; pose K := (lin01 @: fullv)%VS.
+  have memK y: reflect (exists yy, y = in01 yy) (y \in K).
+    apply: (iffP memv_imgP) => [[yy _ ->] | [yy ->]];
+      by exists yy; rewrite ?lfunE ?memvf.
+  have algK: is_aspace K.
+    rewrite /is_aspace has_algid1; last first.
+      by apply/memK; exists 1; rewrite rmorph1.
+    apply/prodvP=> _ _ /memK[y1 ->] /memK[y2 ->].
+    by apply/memK; exists (y1 * y2); rewrite rmorphM.
+  have ker_in01: lker lin01 == 0%VS.
+    by apply/lker0P=> y1 y2; rewrite !lfunE; apply: fmorph_inj.
+  pose f := (lin01 \o linfun (Saut mu0) \o lin01^-1)%VF.
+  have Df y: f (in01 y) = in01 (Saut mu0 y).
+    transitivity (f (lin01 y)); first by rewrite !lfunE.
+    by do 4!rewrite lfunE /=; rewrite lker0_lfunK.
+  have hom_f: kHom 1 (ASpace algK) f.
+    apply/kHomP; split=> [_ _ /memK[y1 ->] /memK[y2 ->] |_ /vlineP[a ->]].
+      by rewrite -rmorphM !Df !rmorphM.
+    by rewrite -(rmorph1 in01) -linearZ /= Df {1}linearZ /= rmorph1.
+  pose pr := map_poly (in_alg Qr) p.
+  have Qpr: pr \is a polyOver 1%VS.
+    by apply/polyOverP=> i; rewrite coef_map memvZ ?memv_line.
+  have splitQr: splittingFieldFor K pr fullv.
+    apply: splittingFieldForS (sub1v (Sub K algK)) (subvf _) _; exists rr => //.
+    congr (_ %= _): (eqpxx pr); apply: (@map_poly_inj _ _ QrC).
+    rewrite Sinj_poly Dr -Drr big_map rmorph_prod; apply: eq_bigr => zz _.
+    by rewrite rmorphB /= map_polyX map_polyC.
+  have [f1 aut_f1 Df1]:= kHom_extends (sub1v (ASpace algK)) hom_f Qpr splitQr.
+  pose nu := LRMorphism (kHom_lrmorphism aut_f1).
+  exists (SubAut Qr QrC nu) => //; exists in01 => //= y.
+  by rewrite -Df -Df1 //; apply/memK; exists y.
+have phiZ: scalable phi.
+  move=> a y; do 2!rewrite -mulr_algl -in_algE.
+  by rewrite -[a]divq_num_den !(fmorph_div, rmorphM, rmorph_int).
+pose fix ext n :=
+  if n is i.+1 then oapp (fun x => s2val (ext1 (ext i) x)) (ext i) (unpickle i)
+  else SubAut Qs QsC (AddLRMorphism phiZ).
+have mem_ext x n: (pickle x < n)%N -> {xx | Sinj (ext n) xx = x}.
+  move=> ltxn; apply: sig_eqW; elim: n ltxn => // n IHn.
+  rewrite ltnS leq_eqVlt => /predU1P[<- | /IHn[xx <-]] /=.
+    by rewrite pickleK /=; case: (ext1 _ x) => mu [xx]; exists xx.
+  case: (unpickle n) => /= [y|]; last by exists xx.
+  case: (ext1 _ y) => mu /= _ [in_mu inj_in_mu _].
+  by exists (in_mu xx); rewrite inj_in_mu.
+pose nu x := Sinj _ (Saut _ (sval (mem_ext x _ (ltnSn _)))).
+have nu_inj n y: nu (Sinj (ext n) y) = Sinj (ext n) (Saut (ext n) y).
+  rewrite /nu; case: (mem_ext _ _ _); move: _.+1 => n1 y1 Dy /=.
+  without loss /subnK Dn1: n n1 y y1 Dy / (n <= n1)%N.
+    by move=> IH; case/orP: (leq_total n n1) => /IH => [/(_ y) | /(_ y1)]->.
+  elim: {n}(_ - n)%N {-1}n => [|k IHk] n in Dn1 y Dy *.
+    by move: y1 Dy; rewrite -Dn1 => y1  /fmorph_inj ->.
+  rewrite addSnnS in Dn1; move/IHk: Dn1 => /=.
+  case: (unpickle _) => [z|] /=; last exact.
+  case: (ext1 _ _) => mu /= _ [in_mu Dinj Daut].
+  by rewrite Dy => /(_ _ (Dinj _))->; rewrite -Daut Dinj.
+suffices nuM: rmorphism nu.
+  by exists (RMorphism nuM) => x; rewrite /= (nu_inj 0%N).
+pose le_nu (x : algC) n := (pickle x < n)%N.
+have max3 x1 x2 x3: exists n, [/\ le_nu x1 n, le_nu x2 n & le_nu x3 n].
+  exists (maxn (pickle x1) (maxn (pickle x2) (pickle x3))).+1.
+  by apply/and3P; rewrite /le_nu !ltnS -!geq_max.
+do 2?split; try move=> x1 x2.
+- have [n] := max3 (x1 - x2) x1 x2.
+  case=> /mem_ext[y Dx] /mem_ext[y1 Dx1] /mem_ext[y2 Dx2].
+  rewrite -Dx nu_inj; rewrite -Dx1 -Dx2 -rmorphB in Dx.
+  by rewrite (fmorph_inj _ Dx) !rmorphB -!nu_inj Dx1 Dx2.
+- have [n] := max3 (x1 * x2) x1 x2.
+  case=> /mem_ext[y Dx] /mem_ext[y1 Dx1] /mem_ext[y2 Dx2].
+  rewrite -Dx nu_inj; rewrite -Dx1 -Dx2 -rmorphM in Dx.
+  by rewrite (fmorph_inj _ Dx) !rmorphM -!nu_inj Dx1 Dx2.
+by rewrite -(rmorph1 QsC) (nu_inj 0%N) !rmorph1.
+Qed.
+
+(* Extended automorphisms of Q_n. *)
+Lemma Qn_aut_exists k n :
+    coprime k n ->
+  {u : {rmorphism algC -> algC} | forall z, z ^+ n = 1 -> u z = z ^+ k}.
+Proof.
+have [-> /eqnP | n_gt0 co_k_n] := posnP n.
+  by rewrite gcdn0 => ->; exists [rmorphism of idfun].
+have [z prim_z] := C_prim_root_exists n_gt0.
+have [Qn [QnC [[|zn []] // [Dz]]] genQn] := num_field_exists [:: z].
+pose phi := kHomExtend 1 \1 zn (zn ^+ k).
+have homQn1: kHom 1 1 (\1%VF : 'End(Qn)) by rewrite kHom1.
+have pzn_zk0: root (map_poly \1%VF (minPoly 1 zn)) (zn ^+ k).
+  rewrite -(fmorph_root QnC) rmorphX Dz -map_poly_comp.
+  rewrite (@eq_map_poly _ _ _ QnC) => [|a]; last by rewrite /= id_lfunE.
+  set p1 := map_poly _ _.
+  have [q1 Dp1]: exists q1, p1 = pQtoC q1.
+    have aP i: (minPoly 1 zn)`_i \in 1%VS.
+      by apply/polyOverP; exact: minPolyOver.
+    have{aP} a_ i := sig_eqW (vlineP _ _ (aP i)).
+    exists (\poly_(i < size (minPoly 1 zn)) sval (a_ i)).
+    apply/polyP=> i; rewrite coef_poly coef_map coef_poly /=.
+    case: ifP => _; rewrite ?rmorph0 //; case: (a_ i) => a /= ->.
+    apply: canRL (mulfK _) _; first by rewrite intr_eq0 denq_eq0.
+    by rewrite mulrzr -rmorphMz scalerMzl -mulrzr -numqE scaler_int rmorph_int.
+  have: root p1 z by rewrite -Dz fmorph_root root_minPoly.
+  rewrite Dp1; have [q2 [Dq2 _] ->] := minCpolyP z.
+  case/dvdpP=> r1 ->; rewrite rmorphM rootM /= -Dq2; apply/orP; right.
+  rewrite (minCpoly_cyclotomic prim_z) /cyclotomic.
+  rewrite (bigD1 (Ordinal (ltn_pmod k n_gt0))) ?coprime_modl //=.
+  by rewrite rootM root_XsubC prim_expr_mod ?eqxx.
+have phiM: lrmorphism phi.
+  by apply/kHom_lrmorphism; rewrite -genQn span_seq1 /= kHomExtendP.
+have [nu Dnu] := extend_algC_subfield_aut QnC (RMorphism phiM).
+exists nu => _ /(prim_rootP prim_z)[i ->].
+rewrite rmorphX exprAC -Dz -Dnu /= -{1}[zn]hornerX /phi.
+rewrite (kHomExtend_poly homQn1) ?polyOverX //.
+rewrite map_polyE map_id_in => [|?]; last by rewrite id_lfunE.
+by rewrite polyseqK hornerX rmorphX.
+Qed.
+
+(* Algebraic integers. *)
+
+Definition Aint : pred_class :=
+  fun x : algC => minCpoly x \is a polyOver Cint.
+Fact Aint_key : pred_key Aint. Proof. by []. Qed.
+Canonical Aint_keyed := KeyedPred Aint_key.
+
+Lemma root_monic_Aint p x :
+  root p x -> p \is monic -> p \is a polyOver Cint -> x \in Aint.
+Proof.
+have pZtoQtoC pz: pQtoC (pZtoQ pz) = pZtoC pz.
+  by rewrite -map_poly_comp; apply: eq_map_poly => b; rewrite /= rmorph_int.
+move=> px0 mon_p /floorCpP[pz Dp]; rewrite unfold_in.
+move: px0; rewrite Dp -pZtoQtoC; have [q [-> mon_q] ->] := minCpolyP x.
+case/dvdpP_rat_int=> qz [a nz_a Dq] [r].
+move/(congr1 (fun q1 => lead_coef (a *: pZtoQ q1))).
+rewrite rmorphM scalerAl -Dq lead_coefZ lead_coefM /=.
+have /monicP->: pZtoQ pz \is monic by rewrite -(map_monic QtoCm) pZtoQtoC -Dp.
+rewrite (monicP mon_q) mul1r mulr1 lead_coef_map_inj //; last exact: intr_inj.
+rewrite Dq => ->; apply/polyOverP=> i; rewrite !(coefZ, coef_map).
+by rewrite -rmorphM /= rmorph_int Cint_int.
+Qed.
+
+Lemma Cint_rat_Aint z : z \in Crat -> z \in Aint -> z \in Cint.
+Proof.
+case/CratP=> a ->{z} /polyOverP/(_ 0%N).
+have [p [Dp mon_p] dv_p] := minCpolyP (ratr a); rewrite Dp coef_map.
+suffices /eqP->: p == 'X - a%:P by rewrite polyseqXsubC /= rmorphN rpredN.
+rewrite -eqp_monic ?monicXsubC // irredp_XsubC //.
+  by rewrite -(size_map_poly QtoCm) -Dp neq_ltn size_minCpoly orbT.
+by rewrite -dv_p fmorph_root root_XsubC.
+Qed.
+
+Lemma Aint_Cint : {subset Cint <= Aint}.
+Proof.
+move=> x; rewrite -polyOverXsubC.
+by apply: root_monic_Aint; rewrite ?monicXsubC ?root_XsubC.
+Qed.
+
+Lemma Aint_int x : x%:~R \in Aint.
+Proof. by rewrite Aint_Cint ?Cint_int. Qed.
+
+Lemma Aint0 : 0 \in Aint. Proof. exact: (Aint_int 0). Qed.
+Lemma Aint1 : 1 \in Aint. Proof. exact: (Aint_int 1). Qed.
+Hint Resolve Aint0 Aint1.
+
+Lemma Aint_unity_root n x : (n > 0)%N -> n.-unity_root x -> x \in Aint.
+Proof.
+move=> n_gt0 xn1; apply: root_monic_Aint xn1 (monic_Xn_sub_1 _ n_gt0) _.
+by apply/polyOverP=> i; rewrite coefB coefC -mulrb coefXn /= rpredB ?rpred_nat.
+Qed.
+
+Lemma Aint_prim_root n z : n.-primitive_root z -> z \in Aint.
+Proof.
+move=> pr_z; apply/(Aint_unity_root (prim_order_gt0 pr_z))/unity_rootP.
+exact: prim_expr_order.
+Qed.
+
+Lemma Aint_Cnat : {subset Cnat <= Aint}.
+Proof. by move=> z /Cint_Cnat/Aint_Cint. Qed.
+
+(* This is Isaacs, Lemma (3.3) *)
+Lemma Aint_subring_exists (X : seq algC) :
+    {subset X <= Aint} ->
+  {S : pred algC &
+     (*a*) subring_closed S
+  /\ (*b*) {subset X <= S}
+   & (*c*) {Y : {n : nat & n.-tuple algC} &
+                {subset tagged Y <= S}
+              & forall x, reflect (inIntSpan (tagged Y) x) (x \in S)}}.
+Proof.
+move=> AZ_X; pose m := (size X).+1.
+pose n (i : 'I_m) := (size (minCpoly X`_i)).-2; pose N := (\max_i n i).+1.
+pose IY := family (fun i => [pred e : 'I_N | e <= n i]%N).
+have IY_0: 0 \in IY by apply/familyP=> // i; rewrite ffunE.
+pose inIY := enum_rank_in IY_0.
+pose Y := [seq \prod_(i < m) X`_i ^+ (f : 'I_N ^ m) i | f in IY].
+have S_P := Cint_spanP [tuple of Y]; set S := Cint_span _ in S_P.
+have sYS: {subset Y <= S} by exact: mem_Cint_span.
+have S_1: 1 \in S.
+  by apply/sYS/imageP; exists 0 => //; rewrite big1 // => i; rewrite ffunE.
+have SmulX (i : 'I_m): {in S, forall x, x * X`_i \in S}.
+  move=> _ /S_P[x ->]; rewrite mulr_suml rpred_sum // => j _.
+  rewrite mulrzAl rpredMz {x}// nth_image mulrC (bigD1 i) //= mulrA -exprS.
+  move: {j}(enum_val j) (familyP (enum_valP j)) => f fP.
+  have:= fP i; rewrite inE /= leq_eqVlt => /predU1P[-> | fi_ltn]; last first.
+    apply/sYS/imageP; have fiK: (inord (f i).+1 : 'I_N) = (f i).+1 :> nat.
+      by rewrite inordK // ltnS (bigmax_sup i).
+    exists (finfun [eta f with i |-> inord (f i).+1]).
+      apply/familyP=> i1; rewrite inE ffunE /= fun_if fiK.
+      by case: eqP => [-> // | _]; exact: fP.
+    rewrite (bigD1 i isT) ffunE /= eqxx fiK; congr (_ * _).
+    by apply: eq_bigr => i1; rewrite ffunE /= => /negPf->.
+  have [/monicP ] := (minCpoly_monic X`_i, root_minCpoly X`_i).
+  rewrite /root horner_coef lead_coefE -(subnKC (size_minCpoly _)) subn2.
+  rewrite big_ord_recr /= addrC addr_eq0 => ->; rewrite mul1r => /eqP->.
+  have /floorCpP[p Dp]: X`_i \in Aint.
+    by have [/(nth_default 0)-> | /(mem_nth 0)/AZ_X] := leqP (size X) i.
+  rewrite -/(n i) Dp mulNr rpredN // mulr_suml rpred_sum // => [[e le_e]] /= _.
+  rewrite coef_map -mulrA mulrzl rpredMz ?sYS //; apply/imageP.
+  have eK: (inord e : 'I_N) = e :> nat by rewrite inordK // ltnS (bigmax_sup i).
+  exists (finfun [eta f with i |-> inord e]).
+    apply/familyP=> i1; rewrite inE ffunE /= fun_if eK.
+    by case: eqP => [-> // | _]; exact: fP.
+  rewrite (bigD1 i isT) ffunE /= eqxx eK; congr (_ * _).
+  by apply: eq_bigr => i1; rewrite ffunE /= => /negPf->.
+exists S; last by exists (Tagged (fun n => n.-tuple _) [tuple of Y]).
+split=> [|x Xx]; last first.
+  by rewrite -[x]mul1r -(nth_index 0 Xx) (SmulX (Ordinal _)) // ltnS index_size.
+split=> // x y Sx Sy; first by rewrite rpredB.
+case/S_P: Sy => {y}[y ->]; rewrite mulr_sumr rpred_sum //= => j.
+rewrite mulrzAr rpredMz {y}// nth_image; move: {j}(enum_val j) => f.
+elim/big_rec: _ => [|i y _ IHy] in x Sx *; first by rewrite mulr1.
+rewrite mulrA {y}IHy //.
+elim: {f}(f i : nat) => [|e IHe] in x Sx *; first by rewrite mulr1.
+by rewrite exprS mulrA IHe // SmulX.
+Qed.
+
+Section AlgIntSubring.
+
+Import DefaultKeying GRing.DefaultPred perm.
+
+(* This is Isaacs, Theorem (3.4). *)
+Theorem fin_Csubring_Aint S n (Y : n.-tuple algC) :
+     mulr_closed S -> (forall x, reflect (inIntSpan Y x) (x \in S)) ->
+  {subset S <= Aint}.
+Proof.
+have ZP_C c: (ZtoC c)%:P \is a polyOver Cint by rewrite raddfMz rpred_int.
+move=> mulS S_P x Sx; pose v := \row_(i < n) Y`_i.
+have [v0 | nz_v] := eqVneq v 0.
+  case/S_P: Sx => {x}x ->; rewrite big1 ?isAlgInt0 // => i _.
+  by have /rowP/(_ i) := v0; rewrite !mxE => ->; rewrite mul0rz.
+have sYS (i : 'I_n): x * Y`_i \in S.
+  by rewrite rpredM //; apply/S_P/Cint_spanP/mem_Cint_span/memt_nth.
+pose A := \matrix_(i, j < n) sval (sig_eqW (S_P _ (sYS j))) i.
+pose p := char_poly (map_mx ZtoC A).
+have: p \is a polyOver Cint.
+  rewrite rpred_sum // => s _; rewrite rpredMsign rpred_prod // => j _.
+  by rewrite !mxE /= rpredB ?rpredMn ?polyOverX.
+apply: root_monic_Aint (char_poly_monic _).
+rewrite -eigenvalue_root_char; apply/eigenvalueP; exists v => //.
+apply/rowP=> j; case dAj: (sig_eqW (S_P _ (sYS j))) => [a DxY].
+by rewrite !mxE DxY; apply: eq_bigr => i _; rewrite !mxE dAj /= mulrzr.
+Qed.
+
+(* This is Isaacs, Corollary (3.5). *)
+Corollary Aint_subring : subring_closed Aint.
+Proof.
+suff rAZ: {in Aint &, forall x y, (x - y \in Aint) * (x * y \in Aint)}.
+  by split=> // x y AZx AZy; rewrite rAZ.
+move=> x y AZx AZy.
+have [|S [ringS] ] := @Aint_subring_exists [:: x; y]; first exact/allP/and3P.
+move=> /allP/and3P[Sx Sy _] [Y _ genYS].
+have AZ_S := fin_Csubring_Aint ringS genYS.
+by have [_ S_B S_M] := ringS; rewrite !AZ_S ?S_B ?S_M.
+Qed.
+Canonical Aint_opprPred := OpprPred Aint_subring.
+Canonical Aint_addrPred := AddrPred Aint_subring.
+Canonical Aint_mulrPred := MulrPred Aint_subring.
+Canonical Aint_zmodPred := ZmodPred Aint_subring.
+Canonical Aint_semiringPred := SemiringPred Aint_subring.
+Canonical Aint_smulrPred := SmulrPred Aint_subring.
+Canonical Aint_subringPred := SubringPred Aint_subring.
+
+End AlgIntSubring.
+
+Lemma Aint_aut (nu : {rmorphism algC -> algC}) x :
+  (nu x \in Aint) = (x \in Aint).
+Proof. by rewrite !unfold_in minCpoly_aut. Qed.
+
+Definition dvdA (e : Algebraics.divisor) : pred_class :=
+  fun z : algC => if e == 0 then z == 0 else z / e \in Aint.
+Fact dvdA_key e : pred_key (dvdA e). Proof. by []. Qed.
+Canonical dvdA_keyed e := KeyedPred (dvdA_key e).
+Delimit Scope algC_scope with A.
+Delimit Scope algC_expanded_scope with Ax.
+Notation "e %| x" := (x \in dvdA e) : algC_expanded_scope.
+Notation "e %| x" := (@in_mem Algebraics.divisor x (mem (dvdA e))) : algC_scope.
+
+Fact dvdA_zmod_closed e : zmod_closed (dvdA e).
+Proof.
+split=> [|x y]; first by rewrite unfold_in mul0r eqxx rpred0 ?if_same.
+rewrite ![(e %| _)%A]unfold_in.
+case: ifP => [_ x0 /eqP-> | _]; first by rewrite subr0.
+by rewrite mulrBl; apply: rpredB.
+Qed.
+Canonical dvdA_opprPred e := OpprPred (dvdA_zmod_closed e).
+Canonical dvdA_addrPred e := AddrPred (dvdA_zmod_closed e).
+Canonical dvdA_zmodPred e := ZmodPred (dvdA_zmod_closed e).
+
+Definition eqAmod (e x y : Algebraics.divisor) := (e %| x - y)%A.
+Notation "x == y %[mod e ]" := (eqAmod e x y) : algC_scope.
+Notation "x != y %[mod e ]" := (~~ (eqAmod e x y)) : algC_scope.
+
+Lemma eqAmod_refl e x : (x == x %[mod e])%A.
+Proof. by rewrite /eqAmod subrr rpred0. Qed.
+Hint Resolve eqAmod_refl.
+
+Lemma eqAmod_sym e x y : ((x == y %[mod e]) = (y == x %[mod e]))%A.
+Proof. by rewrite /eqAmod -opprB rpredN. Qed.
+
+Lemma eqAmod_trans e y x z :
+  (x == y %[mod e] -> y == z %[mod e] -> x == z %[mod e])%A.
+Proof. by move=> Exy Eyz; rewrite /eqAmod -[x](subrK y) -addrA rpredD. Qed.
+
+Lemma eqAmod_transl e x y z :
+  (x == y %[mod e])%A -> (x == z %[mod e])%A = (y == z %[mod e])%A.
+Proof. by move/(sym_left_transitive (eqAmod_sym e) (@eqAmod_trans e)). Qed.
+
+Lemma eqAmod_transr e x y z :
+  (x == y %[mod e])%A -> (z == x %[mod e])%A = (z == y %[mod e])%A.
+Proof. by move/(sym_right_transitive (eqAmod_sym e) (@eqAmod_trans e)). Qed.
+
+Lemma eqAmod0 e x : (x == 0 %[mod e])%A = (e %| x)%A.
+Proof. by rewrite /eqAmod subr0. Qed.
+
+Lemma eqAmodN e x y : (- x == y %[mod e])%A = (x == - y %[mod e])%A.
+Proof. by rewrite eqAmod_sym /eqAmod !opprK addrC. Qed.
+
+Lemma eqAmodDr e x y z : (y + x == z + x %[mod e])%A = (y == z %[mod e])%A.
+Proof. by rewrite /eqAmod addrAC opprD !addrA subrK. Qed.
+
+Lemma eqAmodDl e x y z : (x + y == x + z %[mod e])%A = (y == z %[mod e])%A.
+Proof. by rewrite !(addrC x) eqAmodDr. Qed.
+
+Lemma eqAmodD e x1 x2 y1 y2 :
+  (x1 == x2 %[mod e] -> y1 == y2 %[mod e] -> x1 + y1 == x2 + y2 %[mod e])%A.
+Proof. rewrite -(eqAmodDl e x2 y1) -(eqAmodDr e y1); exact: eqAmod_trans. Qed.
+
+Lemma eqAmodm0 e : (e == 0 %[mod e])%A.
+Proof. by rewrite /eqAmod subr0 unfold_in; case: ifPn => // /divff->. Qed.
+Hint Resolve eqAmodm0.
+
+Lemma eqAmodMr e :
+  {in Aint, forall z x y, x == y %[mod e] -> x * z == y * z %[mod e]}%A.
+Proof.
+move=> z Zz x y.
+rewrite /eqAmod -mulrBl ![(e %| _)%A]unfold_in mulf_eq0 mulrAC.
+by case: ifP => [_ -> // | _ Exy]; apply: rpredM.
+Qed.
+
+Lemma eqAmodMl e :
+  {in Aint, forall z x y, x == y %[mod e] -> z * x == z * y %[mod e]}%A.
+Proof. by move=> z Zz x y Exy; rewrite !(mulrC z) eqAmodMr. Qed.
+
+Lemma eqAmodMl0 e : {in Aint, forall x, x * e == 0 %[mod e]}%A.
+Proof. by move=> x Zx; rewrite -(mulr0 x) eqAmodMl. Qed.
+
+Lemma eqAmodMr0 e : {in Aint, forall x, e * x == 0 %[mod e]}%A.
+Proof. by move=> x Zx; rewrite /= mulrC eqAmodMl0. Qed.
+
+Lemma eqAmod_addl_mul e : {in Aint, forall x y, x * e + y == y %[mod e]}%A.
+Proof. by move=> x Zx y; rewrite -{2}[y]add0r eqAmodDr eqAmodMl0. Qed.
+
+Lemma eqAmodM e : {in Aint &, forall x1 y2 x2 y1,
+  x1 == x2 %[mod e] -> y1 == y2 %[mod e] -> x1 * y1 == x2 * y2 %[mod e]}%A.
+Proof.
+move=> x1 y2 Zx1 Zy2 x2 y1 eq_x /(eqAmodMl Zx1)/eqAmod_trans-> //.
+exact: eqAmodMr.
+Qed.
+
+Lemma eqAmod_rat :
+  {in Crat & &, forall e m n, (m == n %[mod e])%A = (m == n %[mod e])%C}.
+Proof.
+move=> e m n Qe Qm Qn; rewrite /eqCmod unfold_in /eqAmod unfold_in.
+case: ifPn => // nz_e; apply/idP/idP=> [/Cint_rat_Aint | /Aint_Cint] -> //.
+by rewrite rpred_div ?rpredB.
+Qed.
+
+Lemma eqAmod0_rat : {in Crat &, forall e n, (n == 0 %[mod e])%A = (e %| n)%C}.
+Proof. by move=> e n Qe Qn; rewrite /= eqAmod_rat /eqCmod ?subr0 ?Crat0. Qed.
+
+Lemma eqAmod_nat (e m n : nat) : (m == n %[mod e])%A = (m == n %[mod e])%N.
+Proof. by rewrite eqAmod_rat ?rpred_nat // eqCmod_nat. Qed.
+
+Lemma eqAmod0_nat (e m : nat) : (m == 0 %[mod e])%A = (e %| m)%N.
+Proof. by rewrite eqAmod0_rat ?rpred_nat // dvdC_nat. Qed.
+
+(* Multiplicative order. *)
+
+Definition orderC x :=
+  let p := minCpoly x in
+  oapp val 0%N [pick n : 'I_(2 * size p ^ 2) | p == intrp 'Phi_n].
+
+Notation "#[ x ]" := (orderC x) : C_scope.
+
+Lemma exp_orderC x : x ^+ #[x]%C = 1.
+Proof.
+rewrite /orderC; case: pickP => //= [] [n _] /= /eqP Dp.
+have n_gt0: (0 < n)%N.
+  rewrite lt0n; apply: contraTneq (size_minCpoly x) => n0.
+  by rewrite Dp n0 Cyclotomic0 rmorph1 size_poly1.
+have [z prim_z] := C_prim_root_exists n_gt0.
+rewrite prim_expr_order // -(root_cyclotomic prim_z).
+by rewrite -Cintr_Cyclotomic // -Dp root_minCpoly.
+Qed.
+
+Lemma dvdn_orderC x n : (#[x]%C %| n)%N = (x ^+ n == 1).
+Proof.
+apply/idP/eqP=> [|x_n_1]; first by apply: expr_dvd; apply: exp_orderC.
+have [-> | n_gt0] := posnP n; first by rewrite dvdn0.
+have [m prim_x m_dv_n] := prim_order_exists n_gt0 x_n_1.
+have{n_gt0} m_gt0 := dvdn_gt0 n_gt0 m_dv_n; congr (_ %| n)%N: m_dv_n.
+pose p := minCpoly x; have Dp: p = cyclotomic x m := minCpoly_cyclotomic prim_x.
+rewrite /orderC; case: pickP => /= [k /eqP Dp_k | no_k]; last first.
+  suffices lt_m_2p: (m < 2 * size p ^ 2)%N.
+    have /eqP[] := no_k (Ordinal lt_m_2p).
+    by rewrite /= -/p Dp -Cintr_Cyclotomic.
+  rewrite Dp size_cyclotomic (sqrnD 1) addnAC mulnDr -add1n leq_add //.
+  suffices: (m <= \prod_(q <- primes m | q == 2) q * totient m ^ 2)%N.
+    have [m_even | m_odd] := boolP (2 \in primes m).
+      by rewrite -big_filter filter_pred1_uniq ?primes_uniq // big_seq1.
+    by rewrite big_hasC ?has_pred1 // => /leq_trans-> //; apply: leq_addl.
+  rewrite big_mkcond totientE // -mulnn -!big_split /=.
+  rewrite {1}[m]prod_prime_decomp // prime_decompE big_map /= !big_seq.
+  elim/big_ind2: _ => // [n1 m1 n2 m2 | q]; first exact: leq_mul.
+  rewrite mem_primes => /and3P[q_pr _ q_dv_m].
+  rewrite lognE q_pr m_gt0 q_dv_m /=; move: (logn q _) => k.
+  rewrite !mulnA expnS leq_mul //.
+  case: (ltngtP q) => // [|q_gt2 | ->]; first by rewrite ltnNge prime_gt1.
+    rewrite mul1n mulnAC mulnn -{1}[q]muln1 leq_mul ?expn_gt0 ?prime_gt0 //.
+    by rewrite -(subnKC q_gt2) (ltn_exp2l 1).
+  by rewrite !muln1 -expnS (ltn_exp2l 0).
+have k_prim_x: k.-primitive_root x.
+  have k_gt0: (0 < k)%N.
+    rewrite lt0n; apply: contraTneq (size_minCpoly x) => k0.
+    by rewrite Dp_k k0 Cyclotomic0 rmorph1 size_poly1.
+  have [z prim_z] := C_prim_root_exists k_gt0.
+  rewrite -(root_cyclotomic prim_z) -Cintr_Cyclotomic //.
+  by rewrite -Dp_k root_minCpoly.
+apply/eqP; rewrite eqn_dvd !(@prim_order_dvd _ _ x) //.
+by rewrite !prim_expr_order ?eqxx.
+Qed.