Skip to content

Instantly share code, notes, and snippets.

@CohenCyril

CohenCyril/This-revision-was-meant-to-be-a-local-improvement-to.patch

Created September 9, 2020 11:36
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save CohenCyril/c2c7d87c9677ea757a5b67d56a985fb8 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save CohenCyril/c2c7d87c9677ea757a5b67d56a985fb8 to your computer and use it in GitHub Desktop.
Download ZIP
Introduction of xclass
Raw
This-revision-was-meant-to-be-a-local-improvement-to.patch
From 2924bed46a7576c4e0d8a6a1ff0a18d0c9cf717a Mon Sep 17 00:00:00 2001
From: gonthier <gonthier@305884b8-be16-0410-aa53-a3be2363cef1>
Date: Mon, 19 Mar 2012 21:21:11 +0000
Subject: [PATCH] This revision was meant to be a local improvement to falgbra
<-> galois, but it uncovered a major inefficiency of the processing of packed
class declarations by the Coq kernel, which could only be mitigated by
adjusting the packed class idiom. The problem arises from the interference
of several questionable design choices in the Coq kernel, in particular the
blind maximal sharing of "reductions" (which turn out to be full expansions
here). The diagnosis was prompted by the anomalous behaviour of line 302 of
galois.v, which took over 3 minutes of user time to execute. This line
attempts to use an eqP view on an assumption of the form root p x. This is
convertible to p.[x] == 0, but the unfolding heuristic of Coq causes it to
unfold the definition of (_ == _) in the eqP statement instead, only turning
to Hy once it has reached a head normal form for the (_ == _), and thus
having to unfold root p x to head normal form as well. Though unnecessary, by
itself this should not be a problem, even though we are 9 levels deep in the
hierarchy (eqType >-> fieldExtType). Things break down because the kernel
cannot manage to compare the structurally identical terms that result from
this expansion. These have the form let: Equality.Mixin op _ := let:
Choice.Class bc _ := .... let: FieldExt.Class feb _ _ _ :=
let: FieldExt.Pack _ fec _ := L return FieldExt.class_of L in fec
in feb ... in bc in op. so the problem is not immediately
obvious... until one recalls that non-dependent matches also carry explicit
return type annotations. Thus the term is in fact let: Equality.Mixin op _
:= let: Choice.Class bc _ .... let: FieldExt.Class feb _
_ _ := let: FieldExt.Pack _ fec _ := L return FieldExt.class_of L in
fec return Falgebra.class_of F0 (Phant F0) (FieldExt.sort L) in
feb ... return Equality.class_of (Equality.sort Feq)) := in
bc return rel (Equality.sort Feq) in op. where Feq is the eqType
structure that was passed explicitly to eq_op. Feq is the result of several
type inference refinements, so is is not obtained directly as FieldExt.eqType
F0 L, but rather as a composite Zmodule.eqType (Ring.zmodType
(Lalgebra.ringType (Falgebra.vect_lalgType (FieldExt.FalgType L)))) that
evaluates ot the same normal form as FieldExt.eqType F0 L. If the
comparison was based on this (slightly complicated) version of Feq there
would be no problem. However, to arrive at the chain of lets above the Coq
kernel has had to expand the definition of Feq -- and it then proceeds to
share this expansion maximally across the entire expression. Feq is thus now
a fairly large graph, where each of Zmodule.eqType, Ring.zmodType, etc have
been expanded, and the "base" coercions have been expanded: the class
components are subterms of the top "let:" chain, e.g., the class component of
Feq is the let: Choice.class ... subterm. As the kernel "optimizes" the
comparison of Equality.sort (Equality.Pack <monster record>) =
Equality.sort (Equality.Pack <monster record>) by not evaluating the
projection and comparing all the <monster record> rather that just the sort
field, does so by expanding the (shared) term graph into an (unshared) tree,
and these type constraints occur everywhere inside the let: chain (including
in the invisible lambda binders of the predicates and branch subterms), the
diverging behavior is unsurprising. Note that it is the kernel that
diverges here: evarconv unification has absolutely no problem here, because
it uses a different heuristic which does not allow sharing to interfere with
comparison; indeed, it backtracks over the reduction of the argument of a
blocked match, effectively allowing the expansion to "align" on the topmost
match, without having to expose the others. Our partial workaround to this
conundrum is to replace, as much as possible, unexpanded projections like
Equality.sort with exposed matches. This causes the kernel to evaluate the
projection when it propagates an expanded value for the record, rather than
going into the op-described tailspin. The workaround is only partial because
some explicit constants must remain to let unification find canonical
instances, e.g., the Choice.sort field of Choice.eqType, though fortunately
(in this case) evaluation makes most of these vanish. Alas, the largest
instance (the Equality.sort _)cannot be made to simplify in this way: it is
needed for Canonical Structure unification of, say (x \in pred1 y) with x and
y in a finType, with ?x == ?y. The problem here is that evarconv unifies left
to right in the Coq v5-7 term order, where the predicate came before the
match (the called "case") statement, so it has to infer the eqType for ?x and
?y on the basis of the let: return type. In practice, this means that the
packed class idiom gets two extra lines Let xT := let: Pack T _ _ := cT in
T. Notation xclass := (class : class_of xT). and that the various canonical
"inheritance" instances should now use an explicit cT value for the sort,
xclass for the class, and xT for the tag, e.g., Definition zmodType :=
@Zmodule.Pack cT xclass xT. The fix seems reasonably effective in spite of
these shrotcomings: time for line 302 in galois drops from 167s to 1s user
time, which is more acceptable (but still 2 to 3 orders of magnitude too
slow!).
Other changes in this revision:
- "Lagrange" spelling corrected
- the Falgebra interface now contains the UnitRing interface (as an Falgebra
always has a unitRingType structure -- there is a lemma proving this).
- based fieldExtType on Falgebra rather than Field, as this allows all mixins
to be in Prop.
- added construction of simple field extension from an irreducible polynomial,
used it to remove the separability condition in the proof that splitting
fields are normal.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coqfinitgroup/trunk@3751 305884b8-be16-0410-aa53-a3be2363cef1
---
BGsection1.v | 2 +-
BGsection10.v | 2 +-
BGsection11.v | 2 +-
BGsection12.v | 8 +-
BGsection13.v | 2 +-
BGsection15.v | 2 +-
BGsection2.v | 4 +-
BGsection3.v | 8 +-
BGsection4.v | 10 +-
BGsection5.v | 6 +-
BGsection6.v | 2 +-
BGsection7.v | 2 +-
PFsection1.v | 10 +-
PFsection2.v | 12 +-
PFsection4.v | 2 +-
PFsection5.v | 4 +-
PFsection6.v | 22 +--
PFsection7.v | 4 +-
abelian.v | 2 +-
action.v | 4 +-
alt.v | 2 +-
character.v | 4 +-
choice.v | 10 +-
classfun.v | 10 +-
cyclic.v | 4 +-
eqtype.v | 3 +-
extraspecial.v | 22 +--
extremal.v | 20 +-
falgebra.v | 101 ++++++++--
fieldext.v | 465 ++++++++++++++++++++++++++++----------------
finalg.v | 441 +++++++++++++++++++++--------------------
fingroup.v | 46 ++---
fintype.v | 8 +-
frobenius.v | 8 +-
galgebra.v | 8 +-
galois.v | 207 +++++++++++++-------
hall.v | 22 +--
integral_char.v | 9 +-
maximal.v | 14 +-
orderedalg.v | 244 ++++++++++++-----------
pgroup.v | 16 +-
polydiv.v | 1 -
primitive_action.v | 4 +-
quotient.v | 6 +-
ssralg.v | 188 ++++++++++--------
sylow.v | 10 +-
vcharacter.v | 4 +-
vector.v | 10 +-
wielandt_fixpoint.v | 2 +-
49 files changed, 1176 insertions(+), 823 deletions(-)
diff --git a/BGsection1.v b/BGsection1.v
index c0433a7c..0b202983 100644
--- a/BGsection1.v
+++ b/BGsection1.v
@@ -322,7 +322,7 @@ Proposition coprime_cent_prod gT (A G : {group gT}) :
[~: G, A] * 'C_G(A) = G.
Proof.
move=> nGA; have sRG: [~: G, A] \subset G by rewrite commg_subl.
-rewrite -(LaGrange sRG) coprime_mull => /andP[coRA _] /(solvableS sRG).
+rewrite -(Lagrange sRG) coprime_mull => /andP[coRA _] /(solvableS sRG).
exact: coprimeR_cent_prod.
Qed.
diff --git a/BGsection10.v b/BGsection10.v
index cf16dff1..2ddeda34 100644
--- a/BGsection10.v
+++ b/BGsection10.v
@@ -899,7 +899,7 @@ have{nilM'W} nilW: nilpotent W.
by rewrite (quotientYidr (subset_trans sXW nM'W)) quotient_pgroup.
have{qWWM'} sylWp: p.-Sylow(W) Wp.
rewrite /pHall pcore_pgroup (subset_trans (pcore_sub _ _)) ?subsetIr //=.
- rewrite -(LaGrange_index (subsetIr _ _) (pcore_sub _ _)) pnat_mul //.
+ rewrite -(Lagrange_index (subsetIr _ _) (pcore_sub _ _)) pnat_mul //.
rewrite -(divgS (pcore_sub _ _)) -card_quotient ?normsI ?normG //= -pgroupE.
rewrite (pi_p'group qWWM') //= -(dprod_card (nilpotent_pcoreC p nilM'W)).
by rewrite mulKn ?cardG_gt0 // -pgroupE pcore_pgroup.
diff --git a/BGsection11.v b/BGsection11.v
index a3e804aa..7461c8b9 100644
--- a/BGsection11.v
+++ b/BGsection11.v
@@ -375,7 +375,7 @@ have [Q sylQ nQA]: exists2 Q : {group gT}, q.-Sylow(K) Q & A \subset 'N(Q).
have [sQK qQ q'iQK] := and3P sylQ; have [sKE tauK _]:= and3P hallK.
have{q'iQK} not_cQA: ~~ (A \subset 'C(Q)).
apply: contraL q'iQK => cQA; rewrite p'natE // negbK.
- rewrite -(LaGrange_index (subsetIl K 'C(A))) ?dvdn_mulr ?pdiv_dvd //.
+ rewrite -(Lagrange_index (subsetIl K 'C(A))) ?dvdn_mulr ?pdiv_dvd //.
by rewrite subsetI sQK centsC.
have ntQ: Q :!=: 1 by apply: contraNneq not_cQA => ->; exact: cents1.
have q_dv_K: q %| #|K| := dvdn_trans (pdiv_dvd _) (dvdn_indexg _ _).
diff --git a/BGsection12.v b/BGsection12.v
index 0157fd74..0a087a2c 100644
--- a/BGsection12.v
+++ b/BGsection12.v
@@ -2344,12 +2344,12 @@ have [sRM sRH] := subsetIP sR_MH; have [sH'r rrH not_rH'] := and3P t1Hr.
have bH'r: r \notin \beta(H).
by apply: contra sH'r; rewrite -eq_abH; exact: alpha_sub_sigma.
have sylR_H: r.-Sylow(H) R.
- rewrite pHallE sRH -defH -LaGrangeMr partnM ?cardG_gt0 //.
+ rewrite pHallE sRH -defH -LagrangeMr partnM ?cardG_gt0 //.
rewrite -(card_Hall sylR) part_p'nat ?mul1n ?(pnat_dvd (dvdn_indexg _ _)) //=.
by rewrite (pi_p'nat (pcore_pgroup _ _)).
rewrite inE /= orbC -implyNb eq_abM; apply/implyP=> bM'r.
have sylR_M: r.-Sylow(M) R.
- rewrite pHallE sRM -defM -LaGrangeMr partnM ?cardG_gt0 //.
+ rewrite pHallE sRM -defM -LagrangeMr partnM ?cardG_gt0 //.
rewrite -(card_Hall sylR) part_p'nat ?mul1n ?(pnat_dvd (dvdn_indexg _ _)) //=.
by rewrite (pi_p'nat (pcore_pgroup _ _)).
have rrR: 'r_r(R) = 1%N by rewrite (p_rank_Sylow sylR_H) (eqP rrH).
@@ -2460,7 +2460,7 @@ have [x sYxMs]: exists x, Y :^ x \subset M`_\sigma.
have [H hallH] := Hall_exists \sigma(M) solML.
have [sHM sHL] := subsetIP (pHall_sub hallH).
have hallH_L: \sigma(M).-Hall(L) H.
- rewrite pHallE sHL -defL -LaGrangeMr partnM ?cardG_gt0 //.
+ rewrite pHallE sHL -defL -LagrangeMr partnM ?cardG_gt0 //.
rewrite -(card_Hall hallH) part_p'nat ?mul1n //=.
exact: pnat_dvd (dvdn_indexg _ _) sM'K.
have [x _ sYxH]:= Hall_Jsub (mmax_sol maxL) hallH_L sYL sM_Y.
@@ -2480,7 +2480,7 @@ rewrite (leq_trans (p_rankS p sNHY_L)); last first.
have [P sylP] := Sylow_exists p (M :&: L).
have [_ sPL] := subsetIP (pHall_sub sylP).
have{sPL} sylP_L: p.-Sylow(L) P.
- rewrite pHallE sPL -defL -LaGrangeMr partnM ?cardG_gt0 //.
+ rewrite pHallE sPL -defL -LagrangeMr partnM ?cardG_gt0 //.
rewrite -(card_Hall sylP) part_p'nat ?mul1n //=.
exact: pnat_dvd (dvdn_indexg _ _) p'K.
rewrite -(p_rank_Sylow sylP_L) {P sylP sylP_L}(p_rank_Sylow sylP).
diff --git a/BGsection13.v b/BGsection13.v
index 00f9b37c..9c2e2495 100644
--- a/BGsection13.v
+++ b/BGsection13.v
@@ -731,7 +731,7 @@ have{not_pM'} [R ErR nQR]: exists2 R, R \in 'E_r^1('C_M(P)) & R \subset 'N(Q).
have [sSK nQS]: S \subset K /\ S \subset 'N(Q) := subsetIP (pHall_sub sylS).
have sylS_K: r.-Sylow(K) S.
rewrite pHallE sSK /= -/K -(setIidPr sKM) -defM -group_modl // setIAC.
- rewrite (setIidPr sKM) -LaGrangeMr partnM // -(card_Hall sylS).
+ rewrite (setIidPr sKM) -LagrangeMr partnM // -(card_Hall sylS).
rewrite part_p'nat ?mul1n 1?(pnat_dvd (dvdn_indexg _ _)) //.
by apply: (pi_p'nat bMb); apply: contra sM'r; exact: beta_sub_sigma.
have rC: 'r_r('C_M(P)) > 0 by rewrite p_rank_gt0 (piSg _ piHr) // subsetI sHM.
diff --git a/BGsection15.v b/BGsection15.v
index 712757aa..2f25ef62 100644
--- a/BGsection15.v
+++ b/BGsection15.v
@@ -109,7 +109,7 @@ Proof.
rewrite Hall_pi // /Hall Fcore_sub coprime_pi' ?cardG_gt0 //=.
apply/pnatP=> // p p_pr; apply: contraL => /= piMFp; rewrite -p'natE //.
rewrite -partn_eq1 // -(eqn_pmul2l (part_gt0 p #|M`_\F|)) muln1.
-rewrite -partnM ?cardG_gt0 // LaGrange ?Fcore_sub //.
+rewrite -partnM ?cardG_gt0 // Lagrange ?Fcore_sub //.
rewrite -(card_Hall (nilpotent_pcore_Hall p Fcore_nil)) /=.
by rewrite p_core_Fcore // (card_Hall (Fcore_pcore_Sylow piMFp)).
Qed.
diff --git a/BGsection2.v b/BGsection2.v
index 409de09c..b39dc3e8 100644
--- a/BGsection2.v
+++ b/BGsection2.v
@@ -134,7 +134,7 @@ have irrG := mx_abs_irrW absG.
wlog [L simL _]: / exists2 L, mxsimple rH L & (L <= 1%:M)%MS.
by apply: mxsimple_exists; rewrite ?mxmodule1 //; case: irrG.
have ltHG: H \proper G.
- by rewrite properEcard sHG -(LaGrange sHG) ltn_Pmulr // prime_gt1.
+ by rewrite properEcard sHG -(Lagrange sHG) ltn_Pmulr // prime_gt1.
have dvLH: \rank L %| #|H|.
have absL: mx_absolutely_irreducible (submod_repr (mxsimple_module simL)).
by apply: closF; exact/submod_mx_irr.
@@ -175,7 +175,7 @@ have [|] := prime_subgroupVti ('C_G[W | 'Cl] / H)%G prGH.
rewrite (setIidPl _) ?quotientS ?subsetIl // => /trivgP.
rewrite quotient_sub1 //; last by rewrite subIset // normal_norm.
move/setIidPl; rewrite (setIidPr sHcW) /= => defH.
-rewrite -(LaGrange sHG) -(Clifford_rank_components irrG W) card_sH -defH.
+rewrite -(Lagrange sHG) -(Clifford_rank_components irrG W) card_sH -defH.
rewrite mulnC dvdn_pmul2r // (_ : W :=: L)%MS //; apply/eqmxP.
have sLW: (L <= W)%MS by rewrite PackSocleK component_mx_id.
rewrite andbC sLW; have [modL nzL _] := simL.
diff --git a/BGsection3.v b/BGsection3.v
index cfe2d0ba..337e33c2 100644
--- a/BGsection3.v
+++ b/BGsection3.v
@@ -688,7 +688,7 @@ have [sPH nKP]: P \subset H /\ P \subset 'N(K) by apply/andP; rewrite -subsetI.
have nVP := subset_trans sPH nVH.
have coKP: coprime #|K| #|P| by rewrite coprime_sym (pnat_coprime pP).
have{sylP} sylVP: p.-Sylow(H) (V <*> P).
- rewrite pHallE /= norm_joinEr ?mul_subG //= -defH -!LaGrangeMl.
+ rewrite pHallE /= norm_joinEr ?mul_subG //= -defH -!LagrangeMl.
rewrite partnM // part_pnat_id // -!card_quotient //.
by apply/eqP; congr (_ * _)%N; apply: card_Hall; exact: quotient_pHall.
have [trKP | {sylV sVU nVU}ntKP] := eqVneq [~: K, P] 1.
@@ -1028,7 +1028,7 @@ case cKK: (abelian K); last first.
suffices: q ^ 2 >= #|K / K'| by rewrite leqNgt iK'K.
rewrite -divg_normal // leq_divLR ?cardSg //.
rewrite -(@leq_pmul2l (#|[~: K, R]| ^ 2)) ?expn_gt0 ?cardG_gt0 // mulnA.
- rewrite -expnMn -iKR LaGrange // -mulnn -{2}(cardJg _ x) mul_cardG.
+ rewrite -expnMn -iKR Lagrange // -mulnn -{2}(cardJg _ x) mul_cardG.
by rewrite mulKR_Krx mulnAC leq_pmul2l ?muln_gt0 ?cardG_gt0 ?subset_leq_card.
have tiKcP: 'C_K(P) = 1 by rewrite -defKP coprime_abel_cent_TI.
have{IHsub} abelK: q.-abelem K.
@@ -1154,7 +1154,7 @@ have [cSR | not_cSR]:= boolP (R \subset 'C(S | 'JG)).
move/subset_trans; apply; exact: bigcap_inf.
rewrite -afixJG; move/orbit1P => -> allV1.
have defV1: V1 = V by apply: group_inj; rewrite /= -defV allV1 big_set1.
- case/idPn: oKq2; rewrite -(LaGrange (subsetIl K 'C(V1))).
+ case/idPn: oKq2; rewrite -(Lagrange (subsetIl K 'C(V1))).
rewrite (p_maximal_index qK (maxSK V1 S1)) defV1 /= tiKcV cards1 mul1n.
by rewrite (ltn_exp2l 2 1).
have actsR: [acts R, on S | 'JG] := subset_trans (joing_subr P R) actsPR.
@@ -1212,7 +1212,7 @@ have nVjR: forall Vj, Vj \in S :\: D -> 'C_K(Vj) = [~: K, R].
have abelCKR: q.-abelem 'C_K(R) := abelemS (subsetIl _ _) abelK.
have [qCKR _] := andP abelCKR.
apply/eqP; rewrite eq_sym eqEcard sKRVj -(leq_pmul2r (ltnW q_gt1)).
- rewrite -{1}iKj LaGrange ?subsetIl // -{1}defKR (TI_cardMg tiKRcR).
+ rewrite -{1}iKj Lagrange ?subsetIl // -{1}defKR (TI_cardMg tiKRcR).
rewrite leq_pmul2l ?cardG_gt0 //= (card_pgroup qCKR).
rewrite (leq_exp2l _ 1) // -abelem_cyclic // (forall_inP Z_CK) //.
by rewrite (@p_Sylow _ q) // /pHall subxx indexgg qCKR.
diff --git a/BGsection4.v b/BGsection4.v
index 128459b7..e70af216 100644
--- a/BGsection4.v
+++ b/BGsection4.v
@@ -305,7 +305,7 @@ case/pnElemP=> sAR abelA dimA3; have [pA cAA _] := and3P abelA.
have{nsZR} nZA := subset_trans sAR (normal_norm nsZR).
have sHA: H \subset A := subsetIl A _; have abelH := abelemS sHA abelA.
have geH2: logn p #|H| >= 2.
- rewrite -ltnS -dimA3 -(LaGrange sHA) lognM // -addn1 leq_add2l /= -/H.
+ rewrite -ltnS -dimA3 -(Lagrange sHA) lognM // -addn1 leq_add2l /= -/H.
by rewrite logn_quotient_cent_abelem ?dimZ2.
have{abelH} abelK : p.-abelem K.
by rewrite (cprod_abelem _ (cprodEY _)) 1?centsC ?subsetIr ?abelH.
@@ -334,7 +334,7 @@ have cardA : logn p #|A| <= 2.
by rewrite -rank_abelem // (leq_trans (rankS sAR) rankR).
have cardRA : logn p #|R : A| <= 1.
by rewrite -cRAA logn_quotient_cent_abelem // (normal_norm nAR).
-rewrite -(LaGrange sAR) lognM ?cardG_gt0 //.
+rewrite -(Lagrange sAR) lognM ?cardG_gt0 //.
by apply: (leq_trans (leq_add cardA cardRA)).
Qed.
@@ -384,7 +384,7 @@ have dimS1b: logn p #|R / 'Ohm_1(S)| <= 1.
rewrite (leq_trans (logn_quotient _ _ _)) // -(pfactorK 1 p_pr).
by rewrite dvdn_leq_log ?prime_gt0 // order_dvdn yp1.
rewrite (leq_trans (nil_class_pgroup pR)) // geq_max /= -subn1 leq_subLR.
-by rewrite -(LaGrange sS1R) lognM // -card_quotient // addnC leq_add.
+by rewrite -(Lagrange sS1R) lognM // -card_quotient // addnC leq_add.
Qed.
(* This is B & G, Lemma 4.9. *)
@@ -431,7 +431,7 @@ have [dimRb eRb] : logn p #|R / T| = 3 /\ exponent (R / T) %| p.
have ntRb : (R / T) != 1.
by rewrite -cardG_gt1 (card_pgroup pRb) dimRb (ltn_exp2l 0) ?prime_gt1.
have{dimRb} dimR : logn p #|R| = 4.
- by rewrite -(LaGrange sTR) lognM ?cardG_gt0 // dimT -card_quotient ?dimRb.
+ by rewrite -(Lagrange sTR) lognM ?cardG_gt0 // dimT -card_quotient ?dimRb.
have nsR1R: 'Ohm_1(R) <| R := Ohm_normal 1 R; have [sR1R nR1R] := andP nsR1R.
have pR1: p.-group 'Ohm_1(R) := pgroupS sR1R pR.
have p_odd: odd p by case/even_prime: p_pr p_gt3 => ->.
@@ -1352,7 +1352,7 @@ have pGq: p.-group (G / H).
rewrite /pgroup -(card_isog (third_isog sFH nsFG nsHG)) /= -/F -/(pgroup _ _).
case/dprodP: (nilpotent_pcoreC p nilGq) => /= _ <- _ _.
by rewrite defH quotientMidr quotient_pgroup ?pcore_pgroup.
-rewrite pHallE pcore_sub -(LaGrange sHG) partnM // -card_quotient //=.
+rewrite pHallE pcore_sub -(Lagrange sHG) partnM // -card_quotient //=.
have hallHp': p^'.-Hall(H) 'O_p^'(H).
case p'H: (p^'.-group H).
by rewrite pHallE /= pcore_pgroup_id ?subxx //= part_pnat_id.
diff --git a/BGsection5.v b/BGsection5.v
index f3222aa6..9f141d01 100644
--- a/BGsection5.v
+++ b/BGsection5.v
@@ -223,7 +223,7 @@ have defZ: 'C_W(E) = Z.
rewrite subsetI sZW (centsS sER); last by rewrite centsC -subsetIidl defCRZ.
by rewrite (leq_exp2l _ 1) // -ltnS -dimE properG_ltn_log.
have dimW: logn p #|W| = 2.
- apply/eqP; rewrite -(LaGrange sZW) lognM ?cardG_gt0 // oZ (pfactorK 1) //=.
+ apply/eqP; rewrite -(Lagrange sZW) lognM ?cardG_gt0 // oZ (pfactorK 1) //=.
rewrite -/Z eqSS eqn_leq -{1}defZ logn_quotient_cent_abelem ?dimE // -/W.
by rewrite -divgS // logn_div ?cardSg // subn_gt0 properG_ltn_log.
have abelW: p.-abelem W.
@@ -277,7 +277,7 @@ have{SZ sSSZ maxSZ} not_sST: ~~ (S \subset T).
have tiST: S :&: T :=: 1 by rewrite prime_TIg ?oS.
have defST: S * T = R.
apply/eqP; rewrite eqEcard TI_cardMg ?mul_subG ?subsetIl //=.
- by rewrite mulnC oS -maxT LaGrange ?subsetIl.
+ by rewrite mulnC oS -maxT Lagrange ?subsetIl.
have cRRb: abelian (R / T) by rewrite -defST quotientMidr quotient_abelian.
have sR'T: R^`(1) \subset T by rewrite der1_min ?char_norm.
have TI_SR': S :&: R^`(1) :=: 1.
@@ -452,7 +452,7 @@ have{pS cSS} oLb: #|L / K| = p.
have [_ p_dv_Lb _] := pgroup_pdiv (quotient_pgroup _ pL) ntLb.
apply/eqP; rewrite eqn_leq {p_dv_Lb}(dvdn_leq _ p_dv_Lb) // andbT.
rewrite -divg_normal ?(normalS sKL sLH nsKH) // leq_divLR ?cardSg //= -/K.
- rewrite -(card_lcoset K v) -(LaGrangeI L 'C(S)) -indexgI /= -oCHS /K commGC.
+ rewrite -(card_lcoset K v) -(LagrangeI L 'C(S)) -indexgI /= -oCHS /K commGC.
rewrite {2}defS cent_cycle index_cent1 leq_mul ?subset_leq_card ?setSI //.
by apply/subsetP=> vx; case/imsetP=> x Lx ->; rewrite mem_lcoset mem_commg.
have cycLb: cyclic (L / K) by rewrite prime_cyclic ?oLb.
diff --git a/BGsection6.v b/BGsection6.v
index 8b41d98e..86cf0794 100644
--- a/BGsection6.v
+++ b/BGsection6.v
@@ -101,7 +101,7 @@ have nsG'G: G' <| G := der_normal 1 G; have [sG'G nG'G] := andP nsG'G.
have nsG'p'G: 'O_p^'(G') <| G := char_normal_trans (pcore_char _ _) nsG'G.
have nG'p'G := normal_norm nsG'p'G; have solG' := nilpotent_sol nilG'.
have{nilG'} pGb: p.-group (G / 'O_p^'(G')).
- rewrite /pgroup card_quotient -?(LaGrange_index sG'G (pcore_sub _ _)) //=.
+ rewrite /pgroup card_quotient -?(Lagrange_index sG'G (pcore_sub _ _)) //=.
rewrite pnat_mul // -card_quotient // pnat_id //= -pnatNK.
by case/and3P: (nilpotent_pcore_Hall p^' nilG').
have{pGb} cycGb: cyclic (G / 'O_p^'(G')).
diff --git a/BGsection7.v b/BGsection7.v
index 5d422cc6..2b0dde48 100644
--- a/BGsection7.v
+++ b/BGsection7.v
@@ -896,7 +896,7 @@ wlog Zb: b X Y defX B'b p'Y nYA sYX / b \in Z.
have pP2 := pHall_pgroup sylP2.
have: logn p #|P2 : P1| <= 1.
apply: leq_trans dimPP1; rewrite dvdn_leq_log //.
- rewrite -(dvdn_pmul2l (cardG_gt0 [group of P1])) !LaGrange ?subsetIl //.
+ rewrite -(dvdn_pmul2l (cardG_gt0 [group of P1])) !Lagrange ?subsetIl //.
rewrite -(part_pnat_id pP2) (card_Hall sylP).
by rewrite partn_dvd ?cardSg ?subsetT.
rewrite -(pfactorK 1 p_pr) -pfactor_dvdn ?prime_gt0 // -p_part.
diff --git a/PFsection1.v b/PFsection1.v
index fc0e48a2..d2946e20 100644
--- a/PFsection1.v
+++ b/PFsection1.v
@@ -330,7 +330,7 @@ Proof.
set T := 'I_G['chi_t] => nsHG; have [sHG nHG] := andP nsHG.
apply/cfun_inP=> h Hh; rewrite cfResE ?cfIndE // cfunE sum_cfunE.
apply: (canLR (mulKf (neq0GC H))).
-rewrite mulrA -natrM LaGrange ?sub_inertia //= -/T -cfclass_sum //=.
+rewrite mulrA -natrM Lagrange ?sub_inertia //= -/T -cfclass_sum //=.
rewrite mulr_sumr [s in _ = s]big_mkcond /= (reindex_inj invg_inj).
rewrite (partition_big (conjg_Iirr t) xpredT) //=; apply: eq_bigr => i _.
have [[y Gy chi_i] | not_i_t] := cfclassP _ _ _; last first.
@@ -466,7 +466,7 @@ have [Hg | notHg] := boolP (g \in H); last first.
rewrite !(cfun_on0 (cfInd_normal _ _)) //.
by rewrite -(quotientGK AnH) !(Ng, inE) in notHg.
rewrite !cfIndE ?quotientS //; apply: (canRL (mulKf (neq0GC H))).
-rewrite -(LaGrange AsH) natrM mulrA -card_quotient ?normal_norm //.
+rewrite -(Lagrange AsH) natrM mulrA -card_quotient ?normal_norm //.
rewrite (mulfK (neq0GC _)) mulr_sumr.
rewrite (partition_big _ _ (fun x => (mem_quotient A) x G)) /=.
apply: eq_bigr => _ /morphimP[x Nx Gx ->].
@@ -571,7 +571,7 @@ have [HxH | notHxH] := boolP (x \in H); last first.
move=> y Hy; move/supportP:(support_cfun ('Res[H] 'chi_i1))->=>//.
by rewrite memJ_norm //; apply/(subsetP nHT).
rewrite mulr1 cfIndE // (eq_bigr (fun _ => 'chi_i1 x)).
- rewrite sumr_const -(mulr_natl _ #|T|) mulrA -(LaGrange sHT).
+ rewrite sumr_const -(mulr_natl _ #|T|) mulrA -(Lagrange sHT).
congr (_ *_); rewrite natrM mulrA mulVf ?mul1r //.
by move: (cardG_gt0 H); rewrite -neq0N_neqC;case: #|H|.
move => y Hy;rewrite cfResE ?cfunJgen ?genGid //.
@@ -760,9 +760,9 @@ have I1B: 'chi_i1 1%g ^+ 2 <= #|C : D|%:R.
move/leC_trans; apply.
rewrite -leq_leC // -(index_quotient_eq CBsH) ?normal_norm //.
rewrite -(@leq_pmul2l #|'Z('chi_i2)%CF|) ?cardG_gt0 ?cfcenter_sub //.
- rewrite LaGrange ?quotientS ?cfcenter_sub //.
+ rewrite Lagrange ?quotientS ?cfcenter_sub //.
rewrite -(@leq_pmul2l #|(D / B)%g|) ?cardG_gt0 //.
- rewrite mulnA mulnAC LaGrange ?quotientS //.
+ rewrite mulnA mulnAC Lagrange ?quotientS //.
rewrite mulnC leq_pmul2l ?cardG_gt0 // subset_leq_card //.
exact: subset_trans QsZ ZsC.
have IC': is_char ('Ind[G] 'chi_i1) := cfInd_char G (irr_char i1).
diff --git a/PFsection2.v b/PFsection2.v
index 4f082933..b0e25f16 100644
--- a/PFsection2.v
+++ b/PFsection2.v
@@ -72,7 +72,7 @@ rewrite eqEcard card_rcoset {1}class_supportEr; apply/andP; split.
by rewrite mulSg ?mul_subG ?subsetIl // sub1set ?memJ_norm ?groupV.
have oCg Cx: Cx \in Cg :^: H -> #|Cx| = #|C|.
by case/imsetP=> x _ ->; rewrite cardJg card_rcoset.
-by rewrite (card_uniform_partition oCg partCg) oCgH mulnC LaGrange ?subsetIl.
+by rewrite (card_uniform_partition oCg partCg) oCgH mulnC Lagrange ?subsetIl.
Qed.
Definition is_Dade_signalizer (G L A : {set gT}) (H : gT -> {group gT}) :=
@@ -347,8 +347,8 @@ rewrite sumr_const -index_cent1 mulrC -mulr_natr -!mulrA.
rewrite (eq_bigr (fun xa => alpha a * (phi xa)^*)) => [|xa Fa_xa]; last first.
by rewrite (DadeE _ Aa).
rewrite -big_distrr /= -rmorph_sum; congr (_ * _).
-rewrite mulrC mulrA -natrM mulnC -(LaGrange (subsetIl G 'C[a])).
-rewrite -mulnA mulnCA -(sdprod_card def_Ca) -mulnA LaGrange ?subsetIl //.
+rewrite mulrC mulrA -natrM mulnC -(Lagrange (subsetIl G 'C[a])).
+rewrite -mulnA mulnCA -(sdprod_card def_Ca) -mulnA Lagrange ?subsetIl //.
rewrite mulnA natrM mulfK ?neq0GC // -conjC_nat -rmorphM; congr (_ ^*).
have /andP[tiHa _] := Dade_cover_TI Aa.
rewrite (set_partition_big _ (partition_class_support _ _)) //=.
@@ -608,7 +608,7 @@ transitivity (- aa a / #|L|%:R * \sum_(b \in a ^: L) sumB b); last first.
rewrite -mulrA mulrCA -!mulrA; congr (_ * _).
rewrite -invfM mulrCA -invfM -!natrM; congr (_ / _%:R).
rewrite -(sdprod_card (Dade_set_sdprod dB)) mulnA mulnAC; congr (_ * _)%N.
- by rewrite mulnC LaGrange ?subsetIl.
+ by rewrite mulnC Lagrange ?subsetIl.
rewrite (eq_bigr (fun _ => sumB a)) /= => [|_ /imsetP[x Lx ->]]; last first.
rewrite {1}/sumB (reindex_inj (@conjsg_inj _ x)) /=.
symmetry; apply: eq_big => B.
@@ -633,7 +633,7 @@ have ->: aa2 [set a] a = #|'C_G[a]|%:R.
have [-> // _] := normedTI_memJ_P (notHa0 a) (Dade_cover_TI Aa).
by rewrite inE Gxy.
rewrite mulN1r mulrC mulrA -natrM -(sdprod_card (defCA Aa)).
-rewrite -mulnA card_orbit astab1J LaGrange ?subsetIl // mulnC natrM.
+rewrite -mulnA card_orbit astab1J Lagrange ?subsetIl // mulnC natrM.
rewrite mulrAC mulfK ?neq0GC // mulrC divfK ?neq0GC // opprK.
rewrite (bigID [pred B : {set gT} | a \in B]) /= mulrDl addrA.
apply: canRL (subrK _) _; rewrite -mulNr -sumrN; congr (_ + _ * _).
@@ -659,7 +659,7 @@ suffices ->: aa2 B a = #|'H(B) : 'H(a |: B)|%:R * aa2 (a |: B) a.
rewrite /nn2 cardsU1 notBa exprS mulN1r !mulNr; congr (- _).
rewrite !mulrA; congr (_ * _); rewrite -!mulrA; congr (_ * _).
apply: canLR (mulKf (neq0GC _)) _; apply: canRL (mulfK (neq0GC _)) _ => /=.
- by rewrite -natrM mulnC LaGrange //= Dade_setU1 ?subsetIl.
+ by rewrite -natrM mulnC Lagrange //= Dade_setU1 ?subsetIl.
rewrite /aa2 Dade_setU1 //= -natrM; congr _%:R.
have defMB := Dade_set_sdprod dB; have [_ mulHNB nHNB tiHNB] := sdprodP defMB.
have [sHMB sNMB] := mulG_sub mulHNB; have [La nBa] := setIP Na.
diff --git a/PFsection4.v b/PFsection4.v
index 92372146..607412a3 100644
--- a/PFsection4.v
+++ b/PFsection4.v
@@ -842,7 +842,7 @@ Qed.
Let Dade_indexE : #|L : K| = #|W1|.
Proof.
-move: (LaGrange KsL)=> /eqP; rewrite -{1}(sdprod_card SdP) eqn_mul2l.
+move: (Lagrange KsL)=> /eqP; rewrite -{1}(sdprod_card SdP) eqn_mul2l.
by case: #|K| (cardG_gt0 K)=> //= _ _ /eqP.
Qed.
diff --git a/PFsection5.v b/PFsection5.v
index 9f547193..0c6600ba 100644
--- a/PFsection5.v
+++ b/PFsection5.v
@@ -72,7 +72,7 @@ Lemma sum_Iirr_kerD_square H M :
\sum_(i \in Iirr_kerD H M) 'chi_i 1%g ^+ 2 = #|K : H|%:R * (#|H : M|%:R - 1).
Proof.
move=> nsHK nsMK sMH; have [sHK _] := andP nsHK.
-rewrite mulrBr mulr1 -natrM LaGrange_index // -!sum_Iirr_ker_square //.
+rewrite mulrBr mulr1 -natrM Lagrange_index // -!sum_Iirr_ker_square //.
apply/esym/(canLR (addrK _)); rewrite /= addrC (big_setID (Iirr_ker H)).
by rewrite (setIidPr _) ?Iirr_kerS //.
Qed.
@@ -324,7 +324,7 @@ Lemma sum_seqIndD_square :
H <| L -> M <| L -> M \subset H ->
\sum_(phi <- S) phi 1%g ^+ 2 / '[phi] = #|L : H|%:R * (#|H : M|%:R - 1).
Proof.
-move=> nsHL nsML sMH; rewrite -(LaGrange_index sKL sHK) natrM -/e -mulrA.
+move=> nsHL nsML sMH; rewrite -(Lagrange_index sKL sHK) natrM -/e -mulrA.
rewrite -sum_Iirr_kerD_square ?(normalS _ sKL) ?(subset_trans sMH) //.
pose h i := @Ordinal (size S).+1 _ (index_size ('Ind 'chi[K]_i) S).
rewrite (partition_big h (ltn^~ (size S))) => /= [|i Xi]; last first.
diff --git a/PFsection6.v b/PFsection6.v
index 3154bbfa..039b037c 100644
--- a/PFsection6.v
+++ b/PFsection6.v
@@ -118,7 +118,7 @@ rewrite realC_ltNge /isRealC ?rmorphB ?rmorph1 ?rmorph_nat //; last first.
by rewrite posC_conjK ?posC_mul ?posC_nat // Spos ?(sSS SBpsi).
apply: contra not_ineq => /leC_trans-> //.
rewrite -mulrA leC_pmul2l -?(ltn_ltC 0) // def_psi cfInd1 //.
-rewrite -(LaGrange_index sKL sCK) natrM -mulrA leC_pmul2l ?sposGiC //.
+rewrite -(Lagrange_index sKL sCK) natrM -mulrA leC_pmul2l ?sposGiC //.
exact: irr1_bound_quo sDbZC.
Qed.
@@ -165,12 +165,12 @@ have [defA | ltAH] := eqVproper sAH.
by rewrite addn1 defA indexgg in lbHA.
have [sAK ltAK] := (subset_trans sAH sHK, proper_sub_trans ltAH sHK).
case: (@coherent_seqIndD_bound A B H A) => // /idPn[].
-apply: contraL lbHA; rewrite -ltnNge ltn_ltC -(LaGrange_index sHK sAH) natrM.
+apply: contraL lbHA; rewrite -ltnNge ltn_ltC -(Lagrange_index sHK sAH) natrM.
set x := #|H : A|%:R => ub_x.
have nz_x2: sqrtC x != 0 by rewrite sqrtC_eq0 neq0GiC.
have x2_gt0: 0 < sqrtC x by rewrite ltCE nz_x2 sqrtC_pos posC_nat.
have{ub_x}: sqrtC x - (sqrtC x)^-1 <= (2 * #|L : K|)%:R.
- rewrite -(leC_pmul2r _ _ (sposGiC K H)) -natrM -mulnA LaGrange_index //.
+ rewrite -(leC_pmul2r _ _ (sposGiC K H)) -natrM -mulnA Lagrange_index //.
rewrite natrM -(leC_pmul2r _ _ x2_gt0) mulrC mulrBl mulrBr.
rewrite !mulrA -expr2 sqrtCK divff // (leC_trans _ ub_x) // mulrC.
by rewrite leC_add2l leC_opp mul1r -(leq_leC 1).
@@ -247,12 +247,12 @@ have chiefH1: chief_factor L H1 K.
by apply/subsetP; rewrite setSD ?quotientS.
have dv_H21 := dv_e H2 sH12 sH2K nH2L.
have dv_KH2: #|K : H2| == 1 %[mod e].
- have:= dv_e K sH1K (subxx K) nKL; rewrite -(LaGrange_index sH2K sH12).
+ have:= dv_e K sH1K (subxx K) nKL; rewrite -(Lagrange_index sH2K sH12).
by rewrite -modnMmr (eqP dv_H21) modnMmr muln1.
have odd_iK := dvdn_odd (dvdn_indexg _ _) (oddSg (subset_trans _ sKL) oddL).
have iK_gt1 H3 H4: H4 \proper H3 -> (#|H3 : H4| > 1)%N.
by rewrite indexg_gt1 => /andP[].
- by rewrite -(LaGrange_index sH2K sH12) leq_mul ?mod1e_lb ?odd_iK ?iK_gt1.
+ by rewrite -(Lagrange_index sH2K sH12) leq_mul ?mod1e_lb ?odd_iK ?iK_gt1.
split=> //; have nMK := subset_trans sKL (normal_norm nsML).
have not_abKb: ~~ abelian (K / M).
apply: contra (proper_subn ltMH1) => /derG1P/trivgP.
@@ -415,7 +415,7 @@ have /dvdn_addl <-: p ^ (d chi * 2) %| e ^ 2 * sum_p2d X''.
rewrite -mulnDr -big_cat (eq_big_perm _ defX) -(getNatC_nat (e ^ 2 * _)) /=.
rewrite -def_sum_xi1 // /sum_xi1 sum_seqIndD_square ?normal1 ?sub1G //.
rewrite indexg1 -(natrB _ (cardG_gt0 Z)) -natrM getNatC_nat.
-rewrite -(LaGrange_index sKL sZK) mulnAC dvdn_mull //.
+rewrite -(Lagrange_index sKL sZK) mulnAC dvdn_mull //.
have /p_natP[k defKZ]: p.-nat #|K : Z| by rewrite (pnat_dvd (dvdn_indexg K Z)).
rewrite defKZ dvdn_exp2l // -(leq_exp2l _ _ (prime_gt1 p_pr)) -{k}defKZ.
rewrite leq_leC expnM natrX -d_r ?(leC_trans (irr1_bound r).1) //.
@@ -1622,7 +1622,7 @@ have{caseA_coh12} cohXY: coherent (X ++ Y) L^# tau.
by rewrite -Epsi1 !cfunE !psi1Z.
by rewrite -Epsi1 !cfunE -mulrBr dvdC_mul_sign psi1Z.
apply/dvdCP; exists (- x); first by rewrite isIntC_opp.
- rewrite /a -opprB Dx -(LaGrange sZH) mulnC natrM -!mulNr.
+ rewrite /a -opprB Dx -(Lagrange sZH) mulnC natrM -!mulNr.
by rewrite !mulrA !mulfK ?neq0GC.
pose x1 := '[eta1, 'Res psi1]; pose x := x0 + 1 - x1.
have Zx: isIntC x.
@@ -1647,7 +1647,7 @@ have{caseA_coh12} cohXY: coherent (X ++ Y) L^# tau.
by rewrite cfker1 ?(subsetP kerZk).
by rewrite cfdotZr -chi0_1 cfdot_irr (negPf nzi) mulr0.
split=> //; rewrite vcharD1E !cfunE cfInd1 // uniY // lin_i mulr1.
- rewrite -divgS // -(sdprod_card defL) -(LaGrange sZH) -mulnA mulKn //.
+ rewrite -divgS // -(sdprod_card defL) -(Lagrange sZH) -mulnA mulKn //.
rewrite -natrM subrr sub_vchar //=.
by rewrite (vchar_subset _ sXS) ?seqInd_free.
by rewrite scale_vchar ?isIntC_nat // seqInd_vcharW ?sYS.
@@ -1698,7 +1698,7 @@ have{caseA_coh12} cohXY: coherent (X ++ Y) L^# tau.
by rewrite sqrtCK rmorph_nat -natrM.
have{norm_alpha} ub_norm_alpha: '[tau (alpha i0)] < (#|H : Z| ^ 2).*2%:R.
rewrite norm_alpha -addnn -ltn_ltC ltn_add2r.
- rewrite -divgS // -(sdprod_card defL) -(LaGrange sZH) -mulnA mulKn //.
+ rewrite -divgS // -(sdprod_card defL) -(Lagrange sZH) -mulnA mulKn //.
rewrite ltn_pmul2l //.
have frobL2: [Frobenius L / Z = (H / Z) ><| (W1 / Z)]%g.
apply: (Frobenius_coprime_quotient defL nsZL) => //.
@@ -2160,7 +2160,7 @@ rewrite big_seq posC_add ?posC_sum // => [phi Sphi|].
suffices /(allP (seqInd_char _ _)): phi \in S by [].
rewrite sS1S // !mem_cat; rewrite mem_cat in Sphi.
by case/orP: Sphi => [/mem_rem-> | ->]; rewrite ?orbT.
-rewrite leC_sub -(LaGrange_index sHL sZH) -oW1 natrM mulrC -mulrA.
+rewrite leC_sub -(Lagrange_index sHL sZH) -oW1 natrM mulrC -mulrA.
rewrite uniY ?leC_pmul2l ?sposGC //.
rewrite -(prednK (cardG_gt0 Z)) [zz in zz - 1]mulrSr addrK -natrM.
rewrite Dpsi cfInd1 // -oW1.
@@ -2186,7 +2186,7 @@ have [in_caseA | in_caseB] := boolP caseA.
by rewrite regular_norm_dvd_pred // (subset_trans sW1L) ?normal_norm.
rewrite -(muln1 (4 * _)%N) leq_mul //; last first.
by rewrite expn_gt0 -subn1 subn_gt0 orbF cardG_gt1.
-rewrite -(expnMn 2 _ 2) -(LaGrange_index (der_sub 1 H) sZH') leq_mul //.
+rewrite -(expnMn 2 _ 2) -(Lagrange_index (der_sub 1 H) sZH') leq_mul //.
rewrite -(prednK (indexg_gt0 _ _)) leqW // dvdn_leq //.
by rewrite -subn1 subn_gt0 indexg_gt1 proper_subn.
rewrite Gauss_dvd ?(@pnat_coprime 2) -?odd_2'nat ?(oddSg sW1L) //.
diff --git a/PFsection7.v b/PFsection7.v
index cbc22816..b5e093bf 100644
--- a/PFsection7.v
+++ b/PFsection7.v
@@ -224,7 +224,7 @@ Let nzh : h != 0 := neq0GC H.
Let nze : e != 0 := neq0GiC L H.
Let nzL : #|L|%:R != 0 := neq0GC L.
-Let eh : e * h = #|L|%:R. Proof. by rewrite -natrM mulnC LaGrange. Qed.
+Let eh : e * h = #|L|%:R. Proof. by rewrite -natrM mulnC Lagrange. Qed.
Section InvDadeSeqInd.
@@ -672,7 +672,7 @@ have o_nu i j: i != j -> {in S i & S j, forall xi xj, '[nu i xi, nu j xj] = 0}.
by apply: o_ij => //; exact: cohS.
have /all_and2[nze nzh] i: e_ i != 0 /\ h_ i != 0 by rewrite neq0GiC neq0GC.
have h_gt1 i: 1 < h_ i by rewrite -(ltn_ltC 1) cardG_gt1.
-have eh i: e_ i * h_ i = #|L i|%:R by rewrite -natrM mulnC LaGrange.
+have eh i: e_ i * h_ i = #|L i|%:R by rewrite -natrM mulnC Lagrange.
have def_h1 i: h_ i - 1 = #|A i|%:R.
by rewrite /h_ (cardsD1 1%g) group1 addnC natrD addrK.
have [i1 min_i1]: {i1 | forall i, i != i1 -> h_ i1 + 2%:R <= h_ i}.
diff --git a/abelian.v b/abelian.v
index b67558c3..e12a992e 100644
--- a/abelian.v
+++ b/abelian.v
@@ -1078,7 +1078,7 @@ Lemma p_rank_quotient G H : G \subset 'N(H) -> 'r_p(G) - 'r_p(H) <= 'r_p(G / H).
Proof.
move=> nHG; rewrite leq_subLR.
have [E EpE] := p_rank_witness p G; have{EpE} [sEG abelE <-] := pnElemP EpE.
-rewrite -(LaGrangeI E H) lognM ?cardG_gt0 //.
+rewrite -(LagrangeI E H) lognM ?cardG_gt0 //.
rewrite -card_quotient ?(subset_trans sEG) // leq_add ?logn_le_p_rank // !inE.
by rewrite subsetIr (abelemS (subsetIl E H)).
by rewrite quotientS ?quotient_abelem.
diff --git a/action.v b/action.v
index d208cc29..2985c1d1 100644
--- a/action.v
+++ b/action.v
@@ -776,7 +776,7 @@ Qed.
Lemma card_orbit_in_stab G x :
G \subset D -> (#|orbit to G x| * #|'C_G[x | to]|)%N = #|G|.
-Proof. by move=> sGD; rewrite mulnC card_orbit_in ?LaGrange ?subsetIl. Qed.
+Proof. by move=> sGD; rewrite mulnC card_orbit_in ?Lagrange ?subsetIl. Qed.
Lemma acts_sum_card_orbit G S :
[acts G, on S | to] -> \sum_(T \in orbit to G @: S) #|T| = #|S|.
@@ -983,7 +983,7 @@ Lemma dvdn_orbit G x : #|orbit to G x| %| #|G|.
Proof. by rewrite card_orbit dvdn_indexg. Qed.
Lemma card_orbit_stab G x : (#|orbit to G x| * #|'C_G[x | to]|)%N = #|G|.
-Proof. by rewrite mulnC card_orbit LaGrange ?subsetIl. Qed.
+Proof. by rewrite mulnC card_orbit Lagrange ?subsetIl. Qed.
Lemma actsP A S : reflect {acts A, on S | to} [acts A, on S | to].
Proof.
diff --git a/alt.v b/alt.v
index e3043194..f1d423f8 100644
--- a/alt.v
+++ b/alt.v
@@ -76,7 +76,7 @@ Qed.
Lemma card_Alt : 1 < n -> (2 * #|'Alt_T|)%N = n`!.
Proof.
-by move/Alt_index <-; rewrite mulnC (LaGrange Alt_subset) card_Sym.
+by move/Alt_index <-; rewrite mulnC (Lagrange Alt_subset) card_Sym.
Qed.
Lemma Sym_trans : [transitive^n 'Sym_T, on setT | 'P].
diff --git a/character.v b/character.v
index de2c32ed..d8ab4dec 100644
--- a/character.v
+++ b/character.v
@@ -2027,7 +2027,7 @@ Lemma cfnorm_Res_leqif H phi :
H \subset G ->
'['Res[H] phi] <= #|G : H|%:R * '[phi] ?= iff (phi \in 'CF(G, H)).
Proof.
-move=> sHG; rewrite cfun_onE !cfdotE -(LaGrange sHG) mulnC natrM invfM.
+move=> sHG; rewrite cfun_onE !cfdotE -(Lagrange sHG) mulnC natrM invfM.
rewrite -!mulrA mulVKf -?neq0N_neqC -?lt0n //.
rewrite (@big_setID _ _ _ _ G H) /= (setIidPr sHG) mulrDr addrC.
rewrite (eq_bigr (fun x => phi x * (phi x)^*)) => [|i Hi]; last first.
@@ -2142,7 +2142,7 @@ Lemma cfker_Ind chi :
Proof.
move=> sHG Nchi nzchi; rewrite !cfker_nzcharE ?cfInd_char ?cfInd_eq0 //.
apply/setP=> x; rewrite inE cfIndE // (can2_eq (mulVKf _) (mulKf _)) ?neq0GC //.
-rewrite cfInd1 // mulrA -natrM LaGrange // mulr_natl -sumr_const.
+rewrite cfInd1 // mulrA -natrM Lagrange // mulr_natl -sumr_const.
apply/eqP/bigcapP=> [/normC_sum_upper ker_chiG_x y Gy | ker_chiG_x].
by rewrite mem_conjg inE ker_chiG_x ?groupV // => z _; exact: char1_ge_norm.
by apply: eq_bigr => y /groupVr/ker_chiG_x; rewrite mem_conjgV inE => /eqP.
diff --git a/choice.v b/choice.v
index 983a9962..225ee85d 100644
--- a/choice.v
+++ b/choice.v
@@ -239,12 +239,14 @@ Local Coercion sort : type >-> Sortclass.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c T.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
Definition pack m :=
fun b bT & phant_id (Equality.class bT) b => Pack (@Class T b m) T.
(* Inheritance *)
-Definition eqType := Equality.Pack class cT.
+Definition eqType := @Equality.Pack cT xclass xT.
End ClassDef.
@@ -504,12 +506,14 @@ Local Coercion sort : type >-> Sortclass.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c T.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
Definition pack m :=
fun bT b & phant_id (Choice.class bT) b => Pack (@Class T b m) T.
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
End ClassDef.
diff --git a/classfun.v b/classfun.v
index 0521ed6b..f1bc5d73 100644
--- a/classfun.v
+++ b/classfun.v
@@ -104,7 +104,7 @@ Lemma neq0GiC G B : (#|G : B|)%:R != 0 :> algC.
Proof. by rewrite -neq0N_neqC -lt0n. Qed.
Lemma divgS_C G H : H \subset G -> #|G : H|%:R = #|G|%:R / #|H|%:R :> algC.
-Proof. by move/LaGrange <-; rewrite mulnC natrM mulfK ?neq0GC. Qed.
+Proof. by move/Lagrange <-; rewrite mulnC natrM mulfK ?neq0GC. Qed.
Lemma sposGC G : 0 < #|G|%:R.
Proof. by rewrite -(ltn_ltC 0). Qed.
@@ -1274,7 +1274,7 @@ Lemma cfMorph_iso (rT : finGroupType) G D (f : {morphism D >-> rT}) :
G \subset D -> isometry (@cfMorph _ _ G D f).
Proof.
move=> sGD phi psi; rewrite !cfdotE card_morphim (setIidPr sGD).
-rewrite -(LaGrangeI G ('ker f)) /= mulnC natrM invfM -mulrA.
+rewrite -(LagrangeI G ('ker f)) /= mulnC natrM invfM -mulrA.
congr (_ * _); apply: (canLR (mulKf (neq0GC _))).
rewrite mulr_sumr (partition_big_imset f) /= -morphimEsub //.
apply: eq_bigr => _ /morphimP[x Dx Gx ->].
@@ -1356,7 +1356,7 @@ Qed.
Lemma cfInd1 phi : H \subset G -> 'Ind[G] phi 1%g = #|G : H|%:R * phi 1%g.
Proof.
move=> sHG; rewrite cfIndE //; apply: canLR (mulKf (neq0GC H)) _.
-rewrite mulrA -natrM LaGrange // mulr_natl -sumr_const; apply: eq_bigr => x.
+rewrite mulrA -natrM Lagrange // mulr_natl -sumr_const; apply: eq_bigr => x.
by rewrite conj1g.
Qed.
@@ -1364,7 +1364,7 @@ Lemma cfInd_cfun1 : H <| G -> 'Ind[G, H] 1 = #|G : H|%:R *: '1_H.
Proof.
move=> nsHG; have [sHG nHG] := andP nsHG.
apply/cfunP=> x; rewrite cfIndE // cfunE cfuniE //.
-apply: canLR (mulKf (neq0GC H)) _; rewrite mulrA -natrM LaGrange //.
+apply: canLR (mulKf (neq0GC H)) _; rewrite mulrA -natrM Lagrange //.
rewrite mulr_natl -sumr_const; apply: eq_bigr => y Gy.
by rewrite cfun1E -{1}(normsP nHG y Gy) memJ_conjg.
Qed.
@@ -1372,7 +1372,7 @@ Qed.
Lemma cfnorm_Ind_cfun1 : H <| G -> '['Ind[G, H] 1] = #|G : H|%:R.
Proof.
move=> nsHG; rewrite cfInd_cfun1 // cfnormZ normC_nat cfdot_cfuni // setIid.
-rewrite mulrC -mulrA mulrCA (mulrA _%:R) -natrM LaGrange ?normal_sub //.
+rewrite mulrC -mulrA mulrCA (mulrA _%:R) -natrM Lagrange ?normal_sub //.
by rewrite mulKf ?neq0GC.
Qed.
diff --git a/cyclic.v b/cyclic.v
index 974df8e5..d1989325 100644
--- a/cyclic.v
+++ b/cyclic.v
@@ -313,7 +313,7 @@ Lemma ker_eltm : 'ker (eltm dvd_y_x) = <[x ^+ #[y]]>.
Proof.
apply/eqP; rewrite eq_sym eqEcard cycle_subG 3!inE mem_cycle /= eltmE.
rewrite expg_order eqxx (orderE y) -im_eltm card_morphim setIid -orderE.
-by rewrite orderXdiv ?dvdn_indexg //= leq_divRL ?indexg_gt0 ?LaGrange ?subsetIl.
+by rewrite orderXdiv ?dvdn_indexg //= leq_divRL ?indexg_gt0 ?Lagrange ?subsetIl.
Qed.
Lemma injm_eltm : 'injm (eltm dvd_y_x) = (#[x] %| #[y]).
@@ -340,7 +340,7 @@ apply/subsetP=> X; rewrite in_set1 inE -val_eqE /= eqEcard oam.
case/andP=> sXa /eqP oX; rewrite oX leqnn andbT.
apply/subsetP=> x Xx; case/cycleP: (subsetP sXa _ Xx) => k def_x.
have: (x ^+ m == 1)%g by rewrite -oX -order_dvdn cardSg // gen_subG sub1set.
-rewrite {x Xx}def_x -expgM -order_dvdn -[#[a]](LaGrange sXa) -oX mulnC.
+rewrite {x Xx}def_x -expgM -order_dvdn -[#[a]](Lagrange sXa) -oX mulnC.
rewrite dvdn_pmul2r // mulnK // => /dvdnP[i ->].
by rewrite mulnC expgM groupX // cycle_id.
Qed.
diff --git a/eqtype.v b/eqtype.v
index a9e01746..182b35fc 100644
--- a/eqtype.v
+++ b/eqtype.v
@@ -108,7 +108,8 @@ Section ClassDef.
Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
+
+Definition class := let: Pack _ c _ := cT return class_of cT in c.
Definition pack c := @Pack T c T.
Definition clone := fun c & cT -> T & phant_id (pack c) cT => pack c.
diff --git a/extraspecial.v b/extraspecial.v
index 53052aec..f555c71f 100644
--- a/extraspecial.v
+++ b/extraspecial.v
@@ -235,7 +235,7 @@ have defZ: <[z]> = 'Z(G).
by rewrite (sameP commgP cent1P) cent1C.
have sZ_XY: 'Z(G) \subset <[x]> <*> <[y]>.
by rewrite -defZ cycle_subG groupR // mem_gen // inE cycle_id ?orbT.
-rewrite eqEcard sXY_G /= oG -(LaGrange sZ_XY) oZ leq_pmul2l //.
+rewrite eqEcard sXY_G /= oG -(Lagrange sZ_XY) oZ leq_pmul2l //.
rewrite -card_quotient ?(subset_trans sXY_G) //.
rewrite quotientY ?quotient_cycle ?cycle_subG ?(subsetP nZG) //.
have abelGz: p.-abelem (G / 'Z(G)) by rewrite -defPhiG Phi_quotient_abelem.
@@ -390,7 +390,7 @@ have iYG: #|G : Y| = p.
by rewrite mulKn ?cardG_gt0 //= -oZ cardSg ?(subset_trans (MhoS 1 sUG)).
have oU: #|U| = (p ^ 3)%N.
have nvu := subsetP nvG u Gu; have nvU := subset_trans sUG nvG.
- rewrite -(LaGrange (joing_subr _ _)) -orderE ov mulnC; congr (_ * _)%N.
+ rewrite -(Lagrange (joing_subr _ _)) -orderE ov mulnC; congr (_ * _)%N.
rewrite -card_quotient //= quotientYidr ?cycle_subG //=.
rewrite quotient_cycle // -orderE; apply: nt_prime_order => //.
by rewrite -morphX //= coset_id // (subsetP sZv) // Z_Gp.
@@ -411,14 +411,14 @@ have iC1U (U : {group gT}) x:
rewrite cent1_extraspecial_maximal //; apply: contra not_cUx.
by rewrite inE Gx; exact: subsetP (centS sUG) _.
rewrite {1}mul_cardG setIA (setIidPl sUG) -(p_maximal_index pG maxCx) -!mulnA.
- rewrite !LaGrange ?subsetIl // mulnC dvdn_pmul2l //.
+ rewrite !Lagrange ?subsetIl // mulnC dvdn_pmul2l //.
have [sCxG nCxG] := andP (p_maximal_normal pG maxCx).
by rewrite -norm_joinEl ?cardSg ?join_subG ?(subset_trans sUG).
have oCG (U : {group gT}):
Z \subset U -> U \subset G -> #|'C_G(U)| = (p * #|G : U|)%N.
- elim: {U}_.+1 {-2}U (ltnSn #|U|) => // m IHm U leUm sZU sUG.
have [<- | neZU] := eqVneq Z U.
- by rewrite -oZ LaGrange // (setIidPl _) // centsC subsetIr.
+ by rewrite -oZ Lagrange // (setIidPl _) // centsC subsetIr.
have{neZU} [x Gx not_cUx]: exists2 x, x \in G & x \notin 'C(U).
by apply/subsetPn; rewrite eqEsubset sZU subsetI sUG centsC in neZU.
pose W := 'C_U[x]; have iWU: #|U : W| = p by rewrite iC1U // inE not_cUx.
@@ -437,9 +437,9 @@ have oCG (U : {group gT}):
rewrite -sub_cent1; apply/subsetPn; exists x.
by rewrite inE Gx -sub_cent1 subsetIr.
by rewrite -defU centM cent_cycle inE -sub_cent1 subsetIr in not_cUx.
- apply/eqP; rewrite -(eqn_pmul2r p_gt0) -{1}iCW_CU LaGrange ?setIS ?centS //.
+ apply/eqP; rewrite -(eqn_pmul2r p_gt0) -{1}iCW_CU Lagrange ?setIS ?centS //.
rewrite IHm ?(leq_trans (proper_card ltWU)) //= -/W.
- by rewrite -(LaGrange_index sUG sWU) iWU mulnA.
+ by rewrite -(Lagrange_index sUG sWU) iWU mulnA.
have oCY: #|'C_G(Y)| = (p ^ 2)%N by rewrite oCG // iYG.
have [x cYx notZx]: exists2 x, x \in 'C_G(Y) & x \notin Z.
apply/subsetPn; rewrite proper_subn // properEcard setIS ?centS //=.
@@ -447,7 +447,7 @@ have [x cYx notZx]: exists2 x, x \in 'C_G(Y) & x \notin Z.
have{cYx} [Gx cYx] := setIP cYx; have nZx := subsetP nZG x Gx.
have defCx: 'C_G[x] = Y.
apply/eqP; rewrite eq_sym eqEcard subsetI sYG sub_cent1 cYx /=.
- rewrite -(leq_pmul2r p_gt0) -{2}iYG -(iC1U G x) ?LaGrange ?subsetIl //.
+ rewrite -(leq_pmul2r p_gt0) -{2}iYG -(iC1U G x) ?Lagrange ?subsetIl //.
by rewrite !inE Gx ?andbT in notZx *.
have Yx: x \in Y by rewrite -defCx inE Gx cent1id.
have ox: #[x] = p.
@@ -494,7 +494,7 @@ split=> //; first 2 [by exists [group of <[x]>]].
split=> //; rewrite -defE'; apply/joing_idPl.
by rewrite /= defE' -defPhiG (Phi_joing pG) joingC sub_gen ?subsetU ?MhoS.
have iEG: #|G : E| = (p ^ 2)%N.
- apply/eqP; rewrite -(@eqn_pmul2l #|E|) // LaGrange // -(LaGrange sYG) iYG.
+ apply/eqP; rewrite -(@eqn_pmul2l #|E|) // Lagrange // -(Lagrange sYG) iYG.
by rewrite -(dprod_card defY) -mulnA mulnCA -orderE ox.
pose M := 'C_G(E); exists [group of M] => /=.
have sMG: M \subset G := subsetIl _ _; have pM: p.-group M := pgroupS sMG pG.
@@ -503,7 +503,7 @@ have oM: #|M| = (p ^ 3)%N by rewrite oCG ?iEG.
have defME: M * E = G.
apply/eqP; rewrite eqEcard mulG_subG sMG sEG /= -(leq_pmul2r p_gt0).
rewrite -{2}oZ -defZE /('Z(E)) -{2}(setIidPr sEG) setIAC -mul_cardG /= -/M.
- by rewrite -(LaGrange sEG) mulnAC -mulnA mulnC iEG oM.
+ by rewrite -(Lagrange sEG) mulnAC -mulnA mulnC iEG oM.
have defZM: 'Z(M) = Z.
apply/eqP; rewrite eqEsubset andbC subsetI sZM subIset ?centS ?orbT //=.
by rewrite /Z /('Z(G)) -{2}defME centM setIA setIAC.
@@ -744,7 +744,7 @@ apply/eqP; rewrite eqn_leq; apply/andP; split.
have [sEDDn abelE <-] := pnElemP EprE; have [pE cEE _]:= and3P abelE.
rewrite -(@leq_exp2l 2) // -p_part part_pnat_id // -leq_sqr -expnM -mulnn.
rewrite muln2 doubleS expnS -oDDn -(@leq_pmul2r #|'C_DDn(E)|) ?cardG_gt0 //.
- rewrite {1}(card_subcent_extraspecial pDDn) // mulnCA -mulnA LaGrange //=.
+ rewrite {1}(card_subcent_extraspecial pDDn) // mulnCA -mulnA Lagrange //=.
rewrite mulnAC mulnA leq_pmul2r ?cardG_gt0 // setTI.
have ->: (2 * #|'C(E)| = #|'Z(DDn)| * #|'C(E)|)%N.
by rewrite (card_center_extraspecial pDDn).
@@ -800,7 +800,7 @@ have scE: 'C_Dn(E) = E.
exact: injm_extraspecial (pX1p2n_extraspecial _ _).
rewrite dvdn_leq ?cardG_gt0 // (card_subcent_extraspecial pDn) //=.
rewrite -injm_center // cpairg1_center (setIidPl sZE) oZ.
- rewrite -(dvdn_pmul2l (cardG_gt0 E)) mulnn mulnCA LaGrange //.
+ rewrite -(dvdn_pmul2l (cardG_gt0 E)) mulnn mulnCA Lagrange //.
rewrite card_injm ?card_pX1p2n // -expnS pfactor_dvdn ?expn_gt0 ?cardG_gt0 //.
by rewrite lognX dimE mul2n.
apply/pmaxElemP; split=> [|F E2F sEF]; first by rewrite inE subsetT abelE.
diff --git a/extremal.v b/extremal.v
index 329df8ba..d2904287 100644
--- a/extremal.v
+++ b/extremal.v
@@ -279,7 +279,7 @@ have [cycF ffulF]: cyclic F /\ [faithful F, on 'Ohm_1(G) | [Aut G]].
rewrite pHallE -(card_Hall sylP) oP subsetIl /=.
rewrite -(@eqn_pmul2r #|m0 @* A|) ?cardG_gt0 //; apply/eqP.
rewrite -{1}(card_isog (first_isog _)) card_quotient ?ker_norm //.
- by rewrite LaGrange ?subsetIl // oA im_m0 mulnC card_units_Fp.
+ by rewrite Lagrange ?subsetIl // oA im_m0 mulnC card_units_Fp.
have inj_m0: 'ker_F m0 \subset [1] by rewrite setIC ker_m0_P tiPF.
split; last by rewrite /faithful -ker_m0.
have isogF: F \isog [set: {unit 'F_p}].
@@ -516,7 +516,7 @@ have defZ: 'Z(G) = <[x ^+ p]>.
rewrite 2!cycle_subG !groupX ?cent1id //= centsC cXpY /= -orderE oxp leqNgt.
apply: contra notcGG => gtZr; apply: cyclic_center_factor_abelian.
rewrite (dvdn_prime_cyclic p_pr) // card_quotient //.
- rewrite -(dvdn_pmul2l (cardG_gt0 'Z(G))) LaGrange // oG -def_m dvdn_pmul2r //.
+ rewrite -(dvdn_pmul2l (cardG_gt0 'Z(G))) Lagrange // oG -def_m dvdn_pmul2r //.
case/p_natP: (pgroupS sZG pG) gtZr => k ->.
by rewrite ltn_exp2l // def_n1; exact: dvdn_exp2l.
have Zxr: x ^+ r \in 'Z(G) by rewrite /r def_n expnS expgM defZ mem_cycle.
@@ -1059,7 +1059,7 @@ split.
by case/or3P; move/eqP->; rewrite ?maxMt.
have [sHG nHG]:= andP (p_maximal_normal pG maxH).
have oH: #|H| = q.
- apply: double_inj; rewrite -muln2 -(p_maximal_index pG maxH) LaGrange //.
+ apply: double_inj; rewrite -muln2 -(p_maximal_index pG maxH) Lagrange //.
by rewrite oG -mul2n.
rewrite !(eq_sym (gval H)) -eq_sym !eqEcard oH -orderE ox !oMt // !leqnn.
case sHX: (H \subset X) => //=; case/subsetPn: sHX => t Ht notXt.
@@ -1089,7 +1089,7 @@ have isoMt: {in G :\: X, forall t, <<t ^: G>> \isog 'D_q}.
by rewrite !expg_order !eqxx /= invXX' ?mem_cycle.
rewrite !isoMt //; split=> // C; case/cyclicP=> z ->{C} sCG iCG.
rewrite [X]defU // defU -?cycle_subG //.
-by apply: double_inj; rewrite -muln2 -iCG LaGrange // oG -mul2n.
+by apply: double_inj; rewrite -muln2 -iCG Lagrange // oG -mul2n.
Qed.
Theorem quaternion_structure :
@@ -1223,7 +1223,7 @@ have sMtG: {in G :\: X, forall t, <<t ^: G>> \subset G}.
by move=> t; case/setDP=> Gt _; rewrite gen_subG class_subG.
have oMt: {in G :\: X, forall t, #|<<t ^: G>>| = q}.
move=> t X't; have [Gt notXt] := setDP X't.
- rewrite -defMt // -(LaGrange (joing_subl _ _)) -orderE ox2 -def2r mulnC.
+ rewrite -defMt // -(Lagrange (joing_subl _ _)) -orderE ox2 -def2r mulnC.
congr (_ * r)%N; rewrite -card_quotient /=; last first.
by rewrite defMt // (subset_trans _ (nXiG 2)) ?sMtG.
rewrite joingC quotientYidr ?(subset_trans _ (nXiG 2)) ?cycle_subG //.
@@ -1270,7 +1270,7 @@ rewrite pprodE //; split=> // [|||n_gt3].
by case/or3P=> /eqP->; rewrite ?maxMt.
have [sHG nHG]:= andP (p_maximal_normal pG maxH).
have oH: #|H| = q.
- apply: double_inj; rewrite -muln2 -(p_maximal_index pG maxH) LaGrange //.
+ apply: double_inj; rewrite -muln2 -(p_maximal_index pG maxH) Lagrange //.
by rewrite oG -mul2n.
rewrite !(eq_sym (gval H)) -eq_sym !eqEcard oH -orderE ox !oMt // !leqnn.
case sHX: (H \subset X) => //=; case/subsetPn: sHX => z Hz notXz.
@@ -1286,7 +1286,7 @@ have isoMt: {in G :\: X, forall z, <<z ^: G>> \isog 'Q_q}.
by rewrite X'2 // def_xr !eqxx /= invXX' ?mem_cycle.
rewrite !isoMt //; split=> // C; case/cyclicP=> z ->{C} sCG iCG.
rewrite [X]defU // defU -?cycle_subG //.
-by apply: double_inj; rewrite -muln2 -iCG LaGrange // oG -mul2n.
+by apply: double_inj; rewrite -muln2 -iCG Lagrange // oG -mul2n.
Qed.
Theorem semidihedral_structure :
@@ -1410,7 +1410,7 @@ have sMtG: {in G :\: X, forall t, <<t ^: G>> \subset G}.
by move=> t; case/setDP=> Gt _; rewrite gen_subG class_subG.
have oMt: {in G :\: X, forall t, #|<<t ^: G>>| = q}.
move=> t X't; have [Gt notXt] := setDP X't.
- rewrite -defMt // -(LaGrange (joing_subl _ _)) -orderE ox2 -def2r mulnC.
+ rewrite -defMt // -(Lagrange (joing_subl _ _)) -orderE ox2 -def2r mulnC.
congr (_ * r)%N; rewrite -card_quotient /=; last first.
by rewrite defMt // (subset_trans _ (nXiG 2)) ?sMtG.
rewrite joingC quotientYidr ?(subset_trans _ (nXiG 2)) ?cycle_subG //.
@@ -1465,7 +1465,7 @@ split.
by case/or3P=> /eqP->; rewrite ?maxMt.
have [sHG nHG]:= andP (p_maximal_normal pG maxH).
have oH: #|H| = q.
- apply: double_inj; rewrite -muln2 -(p_maximal_index pG maxH) LaGrange //.
+ apply: double_inj; rewrite -muln2 -(p_maximal_index pG maxH) Lagrange //.
by rewrite oG -mul2n.
rewrite !(eq_sym (gval H)) -eq_sym !eqEcard oH -orderE ox !oMt // !leqnn.
case sHX: (H \subset X) => //=; case/subsetPn: sHX => t Ht notXt.
@@ -1484,7 +1484,7 @@ have invX2X': {in G :\: X, forall t, x ^+ 2 ^ t == x ^- 2}.
rewrite -!expgM def2r -order_dvdn ox xy2 dvdnn eqxx invX2X' //=.
by rewrite andbT /r -(subnKC n_gt3).
case/cyclicP=> z ->{C} sCG iCG; rewrite [X]defU // defU -?cycle_subG //.
-by apply: double_inj; rewrite -muln2 -iCG LaGrange // oG -mul2n.
+by apply: double_inj; rewrite -muln2 -iCG Lagrange // oG -mul2n.
Qed.
End ExtremalStructure.
diff --git a/falgebra.v b/falgebra.v
index a642707a..d2fd9d2b 100644
--- a/falgebra.v
+++ b/falgebra.v
@@ -58,15 +58,42 @@ Import GRing.Theory.
(* Finite dimensional algebra *)
Module Falgebra.
+(* Supply a default unitRing mixin for the default unitAlgType base type. *)
+Section DefaultBase.
+
+Variables (K : fieldType) (A : algType K).
+
+Lemma BaseMixin : Vector.mixin_of A -> GRing.UnitRing.mixin_of A.
+Proof.
+move=> vAm; pose vA := VectType K A vAm.
+pose am u := linfun (u \o* idfun : vA -> vA).
+have amE u v : am u v = v * u by rewrite lfunE.
+pose uam := [pred u | lker (am u) == 0%VS].
+pose vam := [fun u => if u \in uam then (am u)^-1%VF 1 else u].
+have vamKl: {in uam, left_inverse 1 vam *%R}.
+ by move=> u Uu; rewrite /= Uu -amE lker0_lfunVK.
+exists uam vam => // [u Uu | u v [_ uv1] | u /negbTE/= -> //].
+ by apply/(lker0P Uu); rewrite !amE -mulrA vamKl // mul1r mulr1.
+by apply/lker0P=> w1 w2 /(congr1 (am v)); rewrite !amE -!mulrA uv1 !mulr1.
+Qed.
+
+Definition BaseType T :=
+ fun c vAm & phant_id c (GRing.UnitRing.Class (BaseMixin vAm)) =>
+ fun (vT : vectType K) & phant vT
+ & phant_id (Vector.mixin (Vector.class vT)) vAm =>
+ @GRing.UnitRing.Pack T c T.
+
+End DefaultBase.
+
Section ClassDef.
Variable R : ringType.
Implicit Type phR : phant R.
Record class_of A := Class {
- base1 : GRing.Algebra.class_of R A;
+ base1 : GRing.UnitAlgebra.class_of R A;
mixin : Vector.mixin_of (GRing.Lmodule.Pack _ base1 A)
}.
-Local Coercion base1 : class_of >-> GRing.Algebra.class_of.
+Local Coercion base1 : class_of >-> GRing.UnitAlgebra.class_of.
Definition base2 A c := @Vector.Class _ _ (@base1 A c) (mixin c).
Local Coercion base2 : class_of >-> Vector.class_of.
@@ -75,28 +102,36 @@ Local Coercion sort : type >-> Sortclass.
Variables (phR : phant R) (T : Type) (cT : type phR).
Definition class := let: Pack _ c _ := cT return class_of cT in c.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
Definition pack :=
- fun bT b & phant_id (@GRing.Algebra.class R phR bT)
- (b : GRing.Algebra.class_of R T) =>
+ fun bT b & phant_id (@GRing.UnitAlgebra.class R phR bT)
+ (b : GRing.UnitAlgebra.class_of R T) =>
fun mT m & phant_id (@Vector.class R phR mT) (@Vector.Class R T b m) =>
Pack (Phant R) (@Class T b m) T.
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition zmodType := GRing.Zmodule.Pack class cT.
-Definition lmodType := GRing.Lmodule.Pack phR class cT.
-Definition ringType := GRing.Ring.Pack class cT.
-Definition lalgType := GRing.Lalgebra.Pack phR class cT.
-Definition algType := GRing.Algebra.Pack phR class cT.
-Definition vectType := Vector.Pack phR class cT.
-Definition vector_ringType := @Vector.Pack R phR ringType class ringType.
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
+Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT.
+Definition ringType := @GRing.Ring.Pack cT xclass xT.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
+Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass xT.
+Definition algType := @GRing.Algebra.Pack R phR cT xclass xT.
+Definition unitAlgType := @GRing.UnitAlgebra.Pack R phR cT xclass xT.
+Definition vectType := @Vector.Pack R phR cT xclass cT.
+Definition vect_ringType := @GRing.Ring.Pack vectType xclass xT.
+Definition vect_unitRingType := @GRing.UnitRing.Pack vectType xclass xT.
+Definition vect_lalgType := @GRing.Lalgebra.Pack R phR vectType xclass xT.
+Definition vect_algType := @GRing.Algebra.Pack R phR vectType xclass xT.
+Definition vect_unitAlgType := @GRing.UnitAlgebra.Pack R phR vectType xclass xT.
End ClassDef.
Module Exports.
-Coercion base1 : class_of >-> GRing.Algebra.class_of.
+Coercion base1 : class_of >-> GRing.UnitAlgebra.class_of.
Coercion base2 : class_of >-> Vector.class_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
@@ -110,19 +145,28 @@ Coercion lmodType : type>-> GRing.Lmodule.type.
Canonical lmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
+Coercion unitRingType : type >-> GRing.UnitRing.type.
+Canonical unitRingType.
Coercion lalgType : type >-> GRing.Lalgebra.type.
Canonical lalgType.
Coercion algType : type >-> GRing.Algebra.type.
Canonical algType.
+Coercion unitAlgType : type >-> GRing.UnitAlgebra.type.
+Canonical unitAlgType.
Coercion vectType : type >-> Vector.type.
Canonical vectType.
-Canonical vector_ringType.
+Canonical vect_ringType.
+Canonical vect_unitRingType.
+Canonical vect_lalgType.
+Canonical vect_algType.
+Canonical vect_unitAlgType.
Notation FalgType R := (type (Phant R)).
Notation "[ 'FalgType' R 'of' A ]" := (@pack _ (Phant R) A _ _ id _ _ id)
(at level 0, format "[ 'FalgType' R 'of' A ]") : form_scope.
Notation "[ 'FalgType' R 'of' A 'for' vT ]" :=
(@pack _ (Phant R) A _ _ id vT _ idfun)
(at level 0, format "[ 'FalgType' R 'of' A 'for' vT ]") : form_scope.
+Notation FalgUnitRingType T := (@BaseType _ _ T _ _ id _ (Phant T) id).
End Exports.
End Falgebra.
@@ -130,7 +174,7 @@ Export Falgebra.Exports.
Notation "1" := (vline 1) : vspace_scope.
-Canonical matrix_FalgType (R : comRingType) n := [FalgType R of 'M[R]_n.+1].
+Canonical matrix_FalgType (K : fieldType) n := [FalgType K of 'M[K]_n.+1].
Section Proper.
@@ -155,7 +199,6 @@ Implicit Types f g : 'End(aT).
Canonical Falg_fun_ringType := lfun_ringType (FalgType_proper aT).
Canonical Falg_fun_lalgType := lfun_lalgType (FalgType_proper aT).
Canonical Falg_fun_algType := lfun_algType (FalgType_proper aT).
-Canonical Falg_fun_FalgType := [FalgType R of 'End(aT)].
Lemma lfun_mulE f g u : (f * g) u = g (f u). Proof. exact: lfunE. Qed.
Lemma lfun_compE f g : (g \o f)%VF = f * g. Proof. by []. Qed.
@@ -194,6 +237,7 @@ Definition lfun_unitRingMixin :=
UnitRingMixin lfun_mulRVr lfun_mulrRV lfun_unitrP lfun_invr_out.
Canonical lfun_unitRingType := UnitRingType 'End(aT) lfun_unitRingMixin.
Canonical lfun_unitAlgType := [unitAlgType K of 'End(aT)].
+Canonical Falg_fun_FalgType := [FalgType K of 'End(aT)].
Lemma lfun_invE f : lker f == 0%VS -> f^-1%VF = f^-1.
Proof. by rewrite /f^-1 /= /lfun_invr => ->. Qed.
@@ -538,6 +582,29 @@ Canonical subvs_lalgType := Eval hnf in LalgType K (subvs_of A) subvs_scaleAl.
Lemma subvs_scaleAr k (x y : subvs_of A) : k *: (x * y) = x * (k *: y).
Proof. exact/val_inj/scalerAr. Qed.
Canonical subvs_algType := Eval hnf in AlgType K (subvs_of A) subvs_scaleAr.
+
+Canonical subvs_unitRingType := Eval hnf in FalgUnitRingType (subvs_of A).
+Canonical subvs_unitAlgType := Eval hnf in [unitAlgType K of subvs_of A].
Canonical subvs_FalgType := Eval hnf in [FalgType K of subvs_of A].
+Lemma vsval_unitr (w : subvs_of A) :
+ vsval w \is a GRing.unit -> w \is a GRing.unit.
+Proof.
+move=> Uv; have /memv_imgP[v1 Av1 v1w]: algid A \in (amulr (val w) @: A)%VS.
+ apply: subvP (memv_algid A); rewrite -dimv_leqif_sup.
+ rewrite limg_dim_eq // -(capv0 A); congr (_ :&: _)%VS.
+ by apply/eqP/lker0P=> v1 v2; rewrite !lfunE; apply: (mulIr Uv).
+ by rewrite -[V in (_ <= V)%VS]prodv_id limg_amulr prodvSr // -memvE (valP w).
+rewrite lfunE /= in v1w; apply/unitrP; exists (Subvs Av1).
+split; apply: val_inj => //; apply: (mulIr Uv).
+by rewrite /= -mulrA -v1w algidl ?algidr ?(valP w).
+Qed.
+
+Lemma vsval_invr (w : subvs_of A) :
+ vsval w \is a GRing.unit -> val w^-1 = (vsval w)^-1.
+Proof.
+by move=> Uv; apply: (mulIr Uv); rewrite -{4}[w](mulVKr (vsval_unitr Uv)) mulKr.
+Qed.
+(* Note that this implies algid A = 1. *)
+
End SubFalgType.
diff --git a/fieldext.v b/fieldext.v
index 1aed589c..a7247aa3 100644
--- a/fieldext.v
+++ b/fieldext.v
@@ -9,10 +9,10 @@ Require Import poly polydiv mxpoly generic_quotient.
(* interfaces. *)
(* [fieldExtType F of L] == a fieldExt F structure for a type L that has both *)
(* fieldType and FalgType F canonical structures. *)
-(* [fieldExtType F of L for aT] == a fieldExtType F structure for a type aT *)
-(* that has a fieldType canonical structure, given an *)
-(* aT : FalgType F whose ringType projection matches *)
-(* the canonical ringType for F. *)
+(* [fieldExtType F of L for K] == a fieldExtType F structure for a type L *)
+(* that has an FalgType F canonical structure, given *)
+(* a K : fieldType whose unitRingType projection *)
+(* coincides with the canonical unitRingType for F. *)
(* {subfield L} == the type of subfields of L that are also extensions *)
(* of F; since we are in a finite dimensional setting *)
(* these are exactly the F-subalgebras of L, and *)
@@ -56,6 +56,15 @@ Require Import poly polydiv mxpoly generic_quotient.
(* in turn has an extFieldType F0 structure. *)
(* baseVspace V == the subspace of baseFieldType L that coincides *)
(* with V : {vspace L}. *)
+(* --> Some caution muse be exercised when using fieldOver and basFieldType, *)
+(* because these are convertible to L while carrying different Lmodule *)
+(* structures. This means that the safeguards engineered in the ssralg *)
+(* library that normally curb the Coq kernel's inclination to diverge are *)
+(* no longer effectcive, so additional precautions should be taken when *)
+(* matching or rewriting terms of the form a *: u, because Coq may take *)
+(* forever to realize it's dealing with a *: in the wrong structure. The *)
+(* baseField_scaleE and fieldOver_scaleE lemmas should be used to expand *)
+(* or fold such "trans-structure" operations explicitly beforehand. *)
(******************************************************************************)
Set Implicit Arguments.
@@ -70,6 +79,13 @@ Lemma modNp (R : fieldType) (r q : {poly R}) :
((- r) %% q) = (- (r %% q)) :> {poly R}.
Proof. by apply/eqP; rewrite -addr_eq0 -modp_add addNr mod0p. Qed.
+Definition irreducible_poly (R : idomainType) (p : {poly R}) :=
+ (size p > 1) * (forall q, q %| p -> (q %= 1) || (q %= p)) : Prop.
+
+Lemma irredp_neq0 (R : idomainType) (p : {poly R}) :
+ irreducible_poly p -> p != 0.
+Proof. by rewrite -size_poly_eq0 -lt0n => [[/ltnW]]. Qed.
+
(* Finite Dimensional Field Extension *)
Module FieldExt.
@@ -81,111 +97,96 @@ Section FieldExt.
Variable R : ringType.
Record class_of T := Class {
- base1 : Field.class_of T;
- lmod_ext : Lmodule.mixin_of R (Zmodule.Pack base1 T);
- lalg_ext : @Lalgebra.axiom R (Lmodule.Pack _ (Lmodule.Class lmod_ext) T)
- (Ring.mul base1);
- alg_ext : Algebra.axiom (Lalgebra.Pack (Phant R)
- (Lalgebra.Class lalg_ext) T);
- vec_ext : Vector.mixin_of (Lmodule.Pack _ (Lmodule.Class lmod_ext) T)
+ base : Falgebra.class_of R T;
+ comm_ext : commutative (Ring.mul base);
+ idomain_ext : IntegralDomain.axiom (Ring.Pack base T);
+ field_ext : Field.mixin_of (UnitRing.Pack base T)
}.
-Local Coercion base1 : class_of >-> Field.class_of.
-Local Coercion alg_ext : class_of >-> Algebra.axiom.
-Definition base2 T (c : class_of T) :=
- @Falgebra.Class _ _ (Algebra.Class c) (vec_ext c).
-Local Coercion base2 : class_of >-> Falgebra.class_of.
-Definition base3 T (c : class_of T) := @UnitAlgebra.Class _ _ c c.
-Local Coercion base3 : class_of >-> UnitAlgebra.class_of.
+Local Coercion base : class_of >-> Falgebra.class_of.
+
+Section Bases.
+Variables (T : Type) (c : class_of T).
+Definition base1 := ComRing.Class (@comm_ext T c).
+Definition base2 := @ComUnitRing.Class T base1 c.
+Definition base3 := @IntegralDomain.Class T base2 (@idomain_ext T c).
+Definition base4 := @Field.Class T base3 (@field_ext T c).
+End Bases.
+Local Coercion base1 : class_of >-> ComRing.class_of.
+Local Coercion base2 : class_of >-> ComUnitRing.class_of.
+Local Coercion base3 : class_of >-> IntegralDomain.class_of.
+Local Coercion base4 : class_of >-> Field.class_of.
Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variables (phR : phant R) (T : Type) (cT : type phR).
Definition class := let: Pack _ c _ := cT return class_of cT in c.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
Definition pack :=
- fun bT b & phant_id (Field.class bT) (b : Field.class_of T) =>
- fun mT lm lam am vm & phant_id (@Falgebra.class _ phR mT)
- (@Falgebra.Class R T
- (@Algebra.Class R T (@Lalgebra.Class R T b lm lam) am) vm) =>
- Pack (Phant R) (@Class T b lm lam am vm) T.
-
-Lemma AlgebraAxiom (base : Field.class_of T)
- (lmod_ext : Lmodule.mixin_of R (Zmodule.Pack base T))
- (lalg_ext : @Lalgebra.axiom R (Lmodule.Pack _ (Lmodule.Class lmod_ext) T)
- (Ring.mul base)) :
- Algebra.axiom (Lalgebra.Pack (Phant R) (Lalgebra.Class lalg_ext) T).
-Proof.
-move=> c /= x y.
-have Hcom: (commutative (Ring.mul base)) by case: (ComUnitRing.base base).
-by rewrite /mul /= !(Hcom x) scalerAl.
-Qed.
-
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition zmodType := Zmodule.Pack class cT.
-Definition ringType := Ring.Pack class cT.
-Definition unitRingType := UnitRing.Pack class cT.
-Definition comRingType := ComRing.Pack class cT.
-Definition comUnitRingType := ComUnitRing.Pack class cT.
-Definition idomainType := IntegralDomain.Pack class cT.
-Definition fieldType := Field.Pack class cT.
-Definition lmodType := Lmodule.Pack phR class cT.
-Definition lalgType := Lalgebra.Pack phR class cT.
-Definition algType := Algebra.Pack phR class cT.
-Definition unitAlgType := UnitAlgebra.Pack phR class cT.
-Definition vectType := Vector.Pack phR class cT.
-Definition FalgType := Falgebra.Pack phR class cT.
-
-Definition unitRing_FalgType := @UnitRing.Pack FalgType class FalgType.
-Definition comRing_FalgType := @ComRing.Pack FalgType class FalgType.
-Definition comUnitRing_FalgType := @ComUnitRing.Pack FalgType class FalgType.
-Definition idomain_FalgType := @IntegralDomain.Pack FalgType class FalgType.
-Definition field_FalgType := @Field.Pack FalgType class FalgType.
-Definition unitAlg_FalgType := @UnitAlgebra.Pack R phR FalgType class FalgType.
-
-Definition unitRing_vectType := @UnitRing.Pack vectType class vectType.
-Definition comRing_vectType := @ComRing.Pack vectType class vectType.
-Definition comUnitRing_vectType := @ComUnitRing.Pack vectType class vectType.
-Definition idomain_vectType := @IntegralDomain.Pack vectType class vectType.
-Definition field_vectType := @Field.Pack vectType class vectType.
-Definition unitAlg_vectType := @UnitAlgebra.Pack R phR vectType class vectType.
-
-Definition comRing_unitAlgType := @ComRing.Pack unitAlgType class unitAlgType.
-Definition comUnitRing_unitAlgType :=
- @ComUnitRing.Pack unitAlgType class unitAlgType.
-Definition idomain_unitAlgType :=
- @IntegralDomain.Pack unitAlgType class unitAlgType.
-Definition field_unitAlgType := @Field.Pack unitAlgType class unitAlgType.
-
-Definition comRing_algType := @ComRing.Pack algType class algType.
-Definition comUnitRing_algType := @ComUnitRing.Pack algType class algType.
-Definition idomain_algType := @IntegralDomain.Pack algType class algType.
-Definition field_algType := @Field.Pack algType class algType.
-
-Definition comRing_lalgType := @ComRing.Pack lalgType class lalgType.
-Definition comUnitRing_lalgType := @ComUnitRing.Pack lalgType class lalgType.
-Definition idomain_lalgType := @IntegralDomain.Pack lalgType class lalgType.
-Definition field_lalgType := @Field.Pack lalgType class lalgType.
-
-Definition comRing_lmodType := @ComRing.Pack lmodType class lmodType.
-Definition comUnitRing_lmodType := @ComUnitRing.Pack lmodType class lmodType.
-Definition idomain_lmodType := @IntegralDomain.Pack lmodType class lmodType.
-Definition field_lmodType := @Field.Pack lmodType class lmodType.
+ fun (bT : Falgebra.type phR) b
+ & phant_id (Falgebra.class bT : Falgebra.class_of R bT)
+ (b : Falgebra.class_of R T) =>
+ fun mT Cm IDm Fm & phant_id (Field.class mT) (@Field.Class T
+ (@IntegralDomain.Class T (@ComUnitRing.Class T (@ComRing.Class T b
+ Cm) b) IDm) Fm) => Pack (Phant R) (@Class T b Cm IDm Fm) T.
+
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @Ring.Pack cT xclass xT.
+Definition unitRingType := @UnitRing.Pack cT xclass xT.
+Definition comRingType := @ComRing.Pack cT xclass xT.
+Definition comUnitRingType := @ComUnitRing.Pack cT xclass xT.
+Definition idomainType := @IntegralDomain.Pack cT xclass xT.
+Definition fieldType := @Field.Pack cT xclass xT.
+Definition lmodType := @Lmodule.Pack R phR cT xclass xT.
+Definition lalgType := @Lalgebra.Pack R phR cT xclass xT.
+Definition algType := @Algebra.Pack R phR cT xclass xT.
+Definition unitAlgType := @UnitAlgebra.Pack R phR cT xclass xT.
+Definition vectType := @Vector.Pack R phR cT xclass xT.
+Definition FalgType := @Falgebra.Pack R phR cT xclass xT.
+
+Definition Falg_comRingType := @ComRing.Pack FalgType xclass xT.
+Definition Falg_comUnitRingType := @ComUnitRing.Pack FalgType xclass xT.
+Definition Falg_idomainType := @IntegralDomain.Pack FalgType xclass xT.
+Definition Falg_fieldType := @Field.Pack FalgType xclass xT.
+
+Definition vect_comRingType := @ComRing.Pack vectType xclass xT.
+Definition vect_comUnitRingType := @ComUnitRing.Pack vectType xclass xT.
+Definition vect_idomainType := @IntegralDomain.Pack vectType xclass xT.
+Definition vect_fieldType := @Field.Pack vectType xclass xT.
+
+Definition unitAlg_comRingType := @ComRing.Pack unitAlgType xclass xT.
+Definition unitAlg_comUnitRingType := @ComUnitRing.Pack unitAlgType xclass xT.
+Definition unitAlg_idomainType := @IntegralDomain.Pack unitAlgType xclass xT.
+Definition unitAlg_fieldType := @Field.Pack unitAlgType xclass xT.
+
+Definition alg_comRingType := @ComRing.Pack algType xclass xT.
+Definition alg_comUnitRingType := @ComUnitRing.Pack algType xclass xT.
+Definition alg_idomainType := @IntegralDomain.Pack algType xclass xT.
+Definition alg_fieldType := @Field.Pack algType xclass xT.
+
+Definition lalg_comRingType := @ComRing.Pack lalgType xclass xT.
+Definition lalg_comUnitRingType := @ComUnitRing.Pack lalgType xclass xT.
+Definition lalg_idomainType := @IntegralDomain.Pack lalgType xclass xT.
+Definition lalg_fieldType := @Field.Pack lalgType xclass xT.
+
+Definition lmod_comRingType := @ComRing.Pack lmodType xclass xT.
+Definition lmod_comUnitRingType := @ComUnitRing.Pack lmodType xclass xT.
+Definition lmod_idomainType := @IntegralDomain.Pack lmodType xclass xT.
+Definition lmod_fieldType := @Field.Pack lmodType xclass xT.
End FieldExt.
Module Exports.
Coercion sort : type >-> Sortclass.
-Coercion base1 : class_of >-> Field.class_of.
-Coercion lmod_ext : class_of >-> Lmodule.mixin_of.
-Coercion lalg_ext : class_of >-> Lalgebra.axiom.
-Coercion alg_ext : class_of >-> Algebra.axiom.
-Coercion vec_ext : class_of >-> Vector.mixin_of.
-Coercion base2 : class_of >-> Falgebra.class_of.
-Coercion base3 : class_of >-> UnitAlgebra.class_of.
+Bind Scope ring_scope with sort.
+Coercion base : class_of >-> Falgebra.class_of.
+Coercion base4 : class_of >-> Field.class_of.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
@@ -217,49 +218,38 @@ Canonical vectType.
Coercion FalgType : type >-> Falgebra.type.
Canonical FalgType.
-Canonical unitRing_FalgType.
-Canonical comRing_FalgType.
-Canonical comUnitRing_FalgType.
-Canonical idomain_FalgType.
-Canonical field_FalgType.
-Canonical unitAlg_FalgType.
-
-Canonical unitRing_vectType.
-Canonical comRing_vectType.
-Canonical comUnitRing_vectType.
-Canonical idomain_vectType.
-Canonical field_vectType.
-Canonical unitAlg_vectType.
-
-Canonical comRing_unitAlgType.
-Canonical comUnitRing_unitAlgType.
-Canonical idomain_unitAlgType.
-Canonical field_unitAlgType.
-
-Canonical comRing_algType.
-Canonical comUnitRing_algType.
-Canonical idomain_algType.
-Canonical field_algType.
-
-Canonical comRing_lalgType.
-Canonical comUnitRing_lalgType.
-Canonical idomain_lalgType.
-Canonical field_lalgType.
-
-Canonical comRing_lmodType.
-Canonical comUnitRing_lmodType.
-Canonical idomain_lmodType.
-Canonical field_lmodType.
-
-Bind Scope ring_scope with sort.
-
+Canonical Falg_comRingType.
+Canonical Falg_comUnitRingType.
+Canonical Falg_idomainType.
+Canonical Falg_fieldType.
+Canonical vect_comRingType.
+Canonical vect_comUnitRingType.
+Canonical vect_idomainType.
+Canonical vect_fieldType.
+Canonical unitAlg_comRingType.
+Canonical unitAlg_comUnitRingType.
+Canonical unitAlg_idomainType.
+Canonical unitAlg_fieldType.
+Canonical alg_comRingType.
+Canonical alg_comUnitRingType.
+Canonical alg_idomainType.
+Canonical alg_fieldType.
+Canonical lalg_comRingType.
+Canonical lalg_comUnitRingType.
+Canonical lalg_idomainType.
+Canonical lalg_fieldType.
+Canonical lmod_comRingType.
+Canonical lmod_comUnitRingType.
+Canonical lmod_idomainType.
+Canonical lmod_fieldType.
Notation fieldExtType R := (type (Phant R)).
-Notation "[ 'fieldExtType' R 'of' T ]" :=
- (@FieldExt.pack _ (Phant R) T _ _ id _ _ _ _ _ id)
- (at level 0, format "[ 'fieldExtType' R 'of' T ]") : form_scope.
-Notation "[ 'fieldExtType' R 'of' T 'for' aT ]" :=
- (@FieldExt.pack _ (Phant R) T _ _ id aT _ _ _ _ idfun)
- (at level 0, format "[ 'fieldExtType' R 'of' T 'for' aT ]") : form_scope.
+
+Notation "[ 'fieldExtType' F 'of' L ]" :=
+ (@pack _ (Phant F) L _ _ id _ _ _ _ id)
+ (at level 0, format "[ 'fieldExtType' F 'of' L ]") : form_scope.
+Notation "[ 'fieldExtType' F 'of' L 'for' K ]" :=
+ (@FieldExt.pack _ (Phant F) L _ _ id K _ _ _ idfun)
+ (at level 0, format "[ 'fieldExtType' F 'of' L 'for' K ]") : form_scope.
Notation "{ 'subfield' L }" := (@aspace_of _ (FalgType _) (Phant L))
(at level 0, format "{ 'subfield' L }") : type_scope.
@@ -661,34 +651,21 @@ Proof. by apply: (mulIf (algid_neq0 K)); rewrite mul1r algidl ?memv_algid. Qed.
Lemma mem1v : 1 \in K. Proof. by rewrite -algid1 memv_algid. Qed.
Lemma sub1v : (1 <= K)%VS. Proof. exact: mem1v. Qed.
-Lemma memv_exp : forall x i, x \in K -> x ^+ i \in K.
-Proof.
-move => x.
-elim => [|i Hi] Hx; first by rewrite expr0 mem1v.
-by rewrite exprS memv_mul // Hi.
-Qed.
-
-Lemma memv_prodl I r (P : pred I) (vs_ : I -> L) :
- (forall i, P i -> vs_ i \in K) -> \prod_(i <- r | P i) vs_ i \in K.
-Proof.
-by move=> Hp; elim/big_ind: _ => //; [exact: mem1v | exact: memv_mul].
-Qed.
-
Fact vsval_multiplicative : multiplicative (vsval : subvs_of K -> L).
Proof. by split => //=; exact: algid1. Qed.
Canonical vsval_rmorphism := AddRMorphism vsval_multiplicative.
Canonical vsval_lrmorphism := [lrmorphism of (vsval : subvs_of K -> L)].
-Definition subvs_mulC := [comRingMixin of subvs_of K by <:].
-Canonical subvs_comRingType := Eval hnf in ComRingType (subvs_of K) subvs_mulC.
+Lemma vsval_invf (w : subvs_of K) : val w^-1 = (vsval w)^-1.
+Proof.
+have [-> | Uv] := eqVneq w 0; first by rewrite !invr0.
+by apply: vsval_invr; rewrite unitfE.
+Qed.
Fact aspace_divr_closed : divr_closed K.
Proof.
split=> [|u v Ku Kv]; first exact: mem1v.
-have [-> | nz_v] := eqVneq v 0; first by rewrite invr0 mulr0 mem0v.
-suffices /memv_imgP[w Kw ->]: u \in (amulr v @: K)%VS by rewrite lfunE mulfK.
-apply: subvP u Ku; rewrite limg_amulr -dimv_leqif_sup ?dim_cosetv //.
-by rewrite -{2}(prodv_id K) prodvSr.
+by rewrite -(vsval_invf (Subvs Kv)) memv_mul ?subvsP.
Qed.
Canonical aspace_mulrPred := MulrPred aspace_divr_closed.
Canonical aspace_divrPred := DivrPred aspace_divr_closed.
@@ -703,17 +680,22 @@ Canonical aspace_divalgPred := DivalgPred (memv_submod_closed K).
Lemma memv_inv u : (u^-1 \in K) = (u \in K). Proof. exact: rpredV. Qed.
Lemma memv_invl u : u \in K -> u^-1 \in K. Proof. exact: GRing.rpredVr. Qed.
-Definition subvs_unitRingMixin :=
- @GRing.SubType.unitRingMixin _ _ _ _ _ _
- (erefl (subvs_of K)) algid1 (rrefl _).
-Canonical subvs_unitRingType :=
- Eval hnf in UnitRingType (subvs_of K) subvs_unitRingMixin.
+Lemma memv_exp x i : x \in K -> x ^+ i \in K. Proof. exact: rpredX. Qed.
+
+Lemma memv_prodl I r (P : pred I) (vs : I -> L) :
+ (forall i, P i -> vs i \in K) -> \prod_(i <- r | P i) vs i \in K.
+Proof. exact: rpred_prod. Qed.
+
+Definition subvs_mulC := [comRingMixin of subvs_of K by <:].
+Canonical subvs_comRingType := Eval hnf in ComRingType (subvs_of K) subvs_mulC.
Canonical subvs_comUnitRingType := Eval hnf in [comUnitRingType of subvs_of K].
-Canonical subvs_unitAlgType := Eval hnf in [unitAlgType F0 of subvs_of K].
Definition subvs_mul_eq0 := [idomainMixin of subvs_of K by <:].
Canonical subvs_idomainType :=
Eval hnf in IdomainType (subvs_of K) subvs_mul_eq0.
-Definition subvs_fieldMixin := [fieldMixin of subvs_of K by <:].
+Lemma subvs_fieldMixin : GRing.Field.mixin_of subvs_idomainType.
+Proof.
+by move=> w nz_w; rewrite unitrE -val_eqE /= vsval_invf algid1 divff.
+Qed.
Canonical subvs_fieldType :=
Eval hnf in FieldType (subvs_of K) subvs_fieldMixin.
Canonical subvs_fieldExtType := Eval hnf in [fieldExtType F0 of subvs_of K].
@@ -1498,6 +1480,9 @@ Definition fieldOver_lmodMixin :=
Canonical fieldOver_lmodType := LmodType K_F L_F fieldOver_lmodMixin.
+Lemma fieldOver_scaleE a (u : L) : a *: (u : L_F) = vsval a * u.
+Proof. by []. Qed.
+
Fact fieldOver_scaleAl a u v : a *F: (u * v) = (a *F: u) * v.
Proof. exact: mulrA. Qed.
@@ -1619,8 +1604,8 @@ Section BaseField.
Variables (F0 : fieldType) (F : fieldExtType F0) (L : fieldExtType F).
-Definition baseFieldType of phant L : Type := L.
-Notation L0 := (baseFieldType (Phant (FieldExt.sort L))).
+Definition baseField_type of phant L : Type := L.
+Notation L0 := (baseField_type (Phant (FieldExt.sort L))).
Canonical baseField_eqType := [eqType of L0].
Canonical baseField_choiceType := [choiceType of L0].
@@ -1653,6 +1638,9 @@ Definition baseField_lmodMixin :=
Canonical baseField_lmodType := LmodType F0 L0 baseField_lmodMixin.
+Lemma baseField_scaleE a (u : L) : a *: (u : L0) = a%:A *: u.
+Proof. by []. Qed.
+
Fact baseField_scaleAl a (u v : L0) : a *F0: (u * v) = (a *F0: u) * v.
Proof. exact: scalerAl. Qed.
@@ -1767,9 +1755,10 @@ apply/idP/idP=> [/coord_vbasis|/coord_span]->; apply/memv_suml=> i _.
rewrite /(_ *: _) /= /fieldOver_scale; case: (coord _ i _) => /= x.
unlock {1}F1; rewrite mem_baseVspace => /vlineP[{x}x ->].
by rewrite -(@scalerAl F L) mul1r memvZ ?memv_span ?memt_nth.
-move: (coord _ i _) => x; rewrite -[_`_i]mul1r scalerAl.
-apply: (@memvZ _ _ J (Subvs _)); last by rewrite vbasis_mem ?memt_nth.
-by unlock F1; rewrite mem_baseVspace (@memvZ F L) ?mem1v.
+move: (coord _ i _) => x; rewrite -[_`_i]mul1r scalerAl -tnth_nth.
+have F1x: x%:A \in F1.
+ by unlock F1; rewrite mem_baseVspace (@memvZ F L) // mem1v.
+by congr (_ \in J): (memvZ (Subvs F1x) (vbasis_mem (mem_tnth i _))).
Qed.
Lemma ideal_baseAspace (E0 : {subfield L0}) :
@@ -1784,6 +1773,8 @@ Qed.
End BaseField.
+Notation baseFieldType L := (baseField_type (Phant L)).
+
(* Base of fieldOver, finally. *)
Section MoreFieldOver.
@@ -1800,3 +1791,145 @@ Lemma base_aspaceOver (E : {subfield L}) :
Proof. by rewrite -sup_field_ideal; exact: base_idealOver. Qed.
End MoreFieldOver.
+
+Lemma irredp_FAdjoin (F : fieldType) (p : {poly F}) :
+ irreducible_poly p ->
+ {L : fieldExtType F & \dim {:L} = (size p).-1 &
+ {z | root (map_poly (in_alg L) p) z & Fadjoin 1 z = fullv}}.
+Proof.
+case=> p_gt1 irr_p; set n := (size p).-1; pose vL := [vectType F of 'rV_n].
+have Dn: n.+1 = size p := ltn_predK p_gt1.
+have nz_p: p != 0 by rewrite -size_poly_eq0 -Dn.
+suffices [L dimL [toPF [toL toPF_K toL_K]]]:
+ {L : fieldExtType F & \dim {:L} = (size p).-1
+ & {toPF : {linear L -> {poly F}} & {toL : {lrmorphism {poly F} -> L} |
+ cancel toPF toL & forall q, toPF (toL q) = q %% p}}}.
+- exists L => //; pose z := toL 'X; set iota := in_alg _.
+ suffices q_z q: toPF (map_poly iota q).[z] = q %% p.
+ exists z; first by rewrite /root -(can_eq toPF_K) q_z modpp linear0.
+ apply/vspaceP=> x; rewrite memvf; apply/poly_Fadjoin.
+ exists (map_poly iota (toPF x)); split.
+ by apply/polyOverP=> i; rewrite coef_map memvZ ?mem1v.
+ by apply: (can_inj toPF_K); rewrite q_z -toL_K toPF_K.
+ elim/poly_ind: q => [|a q IHq].
+ by rewrite map_poly0 horner0 linear0 mod0p.
+ rewrite rmorphD rmorphM /= map_polyX map_polyC hornerMXaddC linearD /=.
+ rewrite linearZ /= -(rmorph1 toL) toL_K -modp_scalel scale_poly1 modp_add.
+ congr (_ + _); rewrite -toL_K rmorphM /= -/z; congr (toPF (_ * z)).
+ by apply: (can_inj toPF_K); rewrite toL_K.
+pose toL q : vL := poly_rV (q %% p); pose toPF (x : vL) := rVpoly x.
+have toL_K q : toPF (toL q) = q %% p.
+ by rewrite /toPF poly_rV_K // -ltnS Dn ?ltn_modp -?Dn.
+have toPF_K: cancel toPF toL.
+ by move=> x; rewrite /toL modp_small ?rVpolyK // -Dn ltnS size_poly.
+have toPinj := can_inj toPF_K.
+pose mul x y := toL (toPF x * toPF y); pose L1 := toL 1.
+have L1K: toPF L1 = 1 by rewrite toL_K modp_small ?size_poly1.
+have mulC: commutative mul by rewrite /mul => x y; rewrite mulrC.
+have mulA: associative mul.
+ by move=> x y z; apply: toPinj; rewrite -!(mulC z) !toL_K !modp_mul mulrCA.
+have mul1: left_id L1 mul.
+ move=> x; apply: toPinj.
+ by rewrite mulC !toL_K modp_mul mulr1 -toL_K toPF_K.
+have mulD: left_distributive mul +%R.
+ move=> x y z; apply: toPinj; rewrite /toPF raddfD /= -!/(toPF _).
+ by rewrite !toL_K /toPF raddfD mulrDl modp_add.
+have nzL1: L1 != 0 by rewrite -(inj_eq toPinj) L1K /toPF raddf0 oner_eq0.
+pose mulM := ComRingMixin mulA mulC mul1 mulD nzL1.
+pose rL := ComRingType (RingType vL mulM) mulC.
+have mulZl: GRing.Lalgebra.axiom mul.
+ move=> a x y; apply: toPinj; rewrite toL_K /toPF !linearZ /= -!/(toPF _).
+ by rewrite toL_K -scalerAl modp_scalel.
+have mulZr: @GRing.Algebra.axiom _ (LalgType F rL mulZl).
+ by move=> a x y; rewrite !(mulrC x) scalerAl.
+pose aL := AlgType F _ mulZr; pose urL := FalgUnitRingType aL.
+pose uaL := [unitAlgType F of AlgType F urL mulZr].
+pose faL := [FalgType F of uaL].
+have unitE: GRing.Field.mixin_of urL.
+ move=> x nz_x; apply/unitrP; set q := toPF x.
+ have nz_q: q != 0 by rewrite -(inj_eq toPinj) /toPF raddf0 in nz_x.
+ have /Bezout_eq1_coprimepP[u upq1]: coprimep p q.
+ have /orP[|/eqp_size sz_pq] := irr_p _ (dvdp_gcdl p q).
+ by rewrite -size_poly_eq1.
+ have: size (gcdp p q) <= size q by exact: leq_gcdpr.
+ by rewrite sz_pq leqNgt (polySpred nz_p) ltnS size_poly.
+ suffices: x * toL u.2 = 1 by exists (toL u.2); rewrite mulrC.
+ apply: toPinj; rewrite !toL_K -upq1 modp_mul modp_add mulrC.
+ by rewrite modp_mull add0r.
+pose ucrL := [comUnitRingType of ComRingType urL mulC].
+have mul0 := GRing.Field.IdomainMixin unitE.
+pose fL := FieldType (IdomainType ucrL mul0) unitE.
+exists [fieldExtType F of faL for fL]; first by rewrite dimvf; exact: mul1n.
+exists [linear of toPF as @rVpoly _ _].
+suffices toLM: lrmorphism (toL : {poly F} -> aL) by exists (LRMorphism toLM).
+have toLlin: linear toL.
+ by move=> a q1 q2; rewrite -linearP -modp_scalel -modp_add.
+do ?split; try exact: toLlin; move=> q r /=.
+by apply: toPinj; rewrite !toL_K modp_mul -!(mulrC r) modp_mul.
+Qed.
+
+(* Coq 8.3 processes this shorter proof correctly, but then crashes on Qed.
+Lemma irredp_FAdjoin (F : fieldType) (p : {poly F}) :
+ irreducible_poly p ->
+ {L : fieldExtType F & Vector.dim L = (size p).-1 &
+ {z | root (map_poly (in_alg L) p) z & Fadjoin 1 z = fullv}}.
+Proof.
+case=> p_gt1 irr_p; set n := (size p).-1; pose vL := [vectType F of 'rV_n].
+have Dn: n.+1 = size p := ltn_predK p_gt1.
+have nz_p: p != 0 by rewrite -size_poly_eq0 -Dn.
+pose toL q : vL := poly_rV (q %% p).
+have toL_K q : rVpoly (toL q) = q %% p.
+ by rewrite poly_rV_K // -ltnS Dn ?ltn_modp -?Dn.
+pose mul (x y : vL) : vL := toL (rVpoly x * rVpoly y).
+pose L1 : vL := poly_rV 1.
+have L1K: rVpoly L1 = 1 by rewrite poly_rV_K // size_poly1 -ltnS Dn.
+have mulC: commutative mul by rewrite /mul => x y; rewrite mulrC.
+have mulA: associative mul.
+ by move=> x y z; rewrite -!(mulC z) /mul !toL_K /toL !modp_mul mulrCA.
+have mul1: left_id L1 mul.
+ move=> x; rewrite /mul L1K mul1r /toL modp_small ?rVpolyK // -Dn ltnS.
+ by rewrite size_poly.
+have mulD: left_distributive mul +%R.
+ move=> x y z; apply: canLR (@rVpolyK _ _) _.
+ by rewrite !raddfD mulrDl /= !toL_K /toL modp_add.
+have nzL1: L1 != 0 by rewrite -(can_eq (@rVpolyK _ _)) L1K raddf0 oner_eq0.
+pose mulM := ComRingMixin mulA mulC mul1 mulD nzL1.
+pose rL := ComRingType (RingType vL mulM) mulC.
+have mulZl: GRing.Lalgebra.axiom mul.
+ move=> a x y; apply: canRL (@rVpolyK _ _) _; rewrite !linearZ /= toL_K.
+ by rewrite -scalerAl modp_scalel.
+have mulZr: @GRing.Algebra.axiom _ (LalgType F rL mulZl).
+ by move=> a x y; rewrite !(mulrC x) scalerAl.
+pose aL := AlgType F _ mulZr; pose urL := FalgUnitRingType aL.
+pose uaL := [unitAlgType F of AlgType F urL mulZr].
+pose faL := [FalgType F of uaL].
+have unitE: GRing.Field.mixin_of urL.
+ move=> x nz_x; apply/unitrP; set q := rVpoly x.
+ have nz_q: q != 0 by rewrite -(can_eq (@rVpolyK _ _)) raddf0 in nz_x.
+ have /Bezout_eq1_coprimepP[u upq1]: coprimep p q.
+ have /orP[|/eqp_size sz_pq] := irr_p _ (dvdp_gcdl p q).
+ by rewrite -size_poly_eq1.
+ have: size (gcdp p q) <= size q by exact: leq_gcdpr.
+ by rewrite sz_pq leqNgt (polySpred nz_p) ltnS size_poly.
+ suffices: x * toL u.2 = 1 by exists (toL u.2); rewrite mulrC.
+ congr (poly_rV _); rewrite toL_K modp_mul mulrC (canRL (addKr _) upq1).
+ by rewrite -mulNr modp_addl_mul_small ?size_poly1.
+pose ucrL := [comUnitRingType of ComRingType urL mulC].
+pose fL := FieldType (IdomainType ucrL (GRing.Field.IdomainMixin unitE)) unitE.
+exists [fieldExtType F of faL for fL]; first exact: mul1n.
+pose z : vL := toL 'X; set iota := in_alg _.
+have q_z q: rVpoly (map_poly iota q).[z] = q %% p.
+ elim/poly_ind: q => [|a q IHq].
+ by rewrite map_poly0 horner0 linear0 mod0p.
+ rewrite rmorphD rmorphM /= map_polyX map_polyC hornerMXaddC linearD /=.
+ rewrite linearZ /= L1K scale_poly1 modp_add; congr (_ + _); last first.
+ by rewrite modp_small // size_polyC; case: (~~ _) => //; apply: ltnW.
+ by rewrite !toL_K IHq mulrC modp_mul mulrC modp_mul.
+exists z; first by rewrite /root -(can_eq (@rVpolyK _ _)) q_z modpp linear0.
+apply/vspaceP=> x; rewrite memvf; apply/poly_Fadjoin.
+exists (map_poly iota (rVpoly x)); split.
+ by apply/polyOverP=> i; rewrite coef_map memvZ ?mem1v.
+apply: (can_inj (@rVpolyK _ _)).
+by rewrite q_z modp_small // -Dn ltnS size_poly.
+Qed.
+*)
\ No newline at end of file
diff --git a/finalg.v b/finalg.v
index 40f1e590..bab1a0a7 100644
--- a/finalg.v
+++ b/finalg.v
@@ -83,14 +83,16 @@ Local Coercion sort : type >-> Sortclass.
Definition pack := gen_pack Pack Class GRing.Zmodule.class.
Variable cT : type.
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition countType := Countable.Pack (fin_ class) cT.
-Definition finType := Finite.Pack (fin_ class) cT.
-Definition zmodType := GRing.Zmodule.Pack class cT.
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition countType := @Countable.Pack cT (fin_ xclass) xT.
+Definition finType := @Finite.Pack cT (fin_ xclass) xT.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
-Definition join_finType := @Finite.Pack zmodType (fin_ class) cT.
+Definition join_finType := @Finite.Pack zmodType (fin_ xclass) xT.
Definition baseFinGroupType := base_group cT zmodType finType.
Definition finGroupType := fin_group baseFinGroupType zmodType.
@@ -166,16 +168,18 @@ Local Coercion sort : type >-> Sortclass.
Definition pack := gen_pack Pack Class GRing.Ring.class.
Variable cT : type.
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition countType := Countable.Pack (fin_ class) cT.
-Definition finType := Finite.Pack (fin_ class) cT.
-Definition zmodType := GRing.Zmodule.Pack class cT.
-Definition finZmodType := Zmodule.Pack class cT.
-Definition ringType := GRing.Ring.Pack class cT.
-Definition join_finType := @Finite.Pack ringType (fin_ class) cT.
-Definition join_finZmodType := @Zmodule.Pack ringType class cT.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition countType := @Countable.Pack cT (fin_ xclass) xT.
+Definition finType := @Finite.Pack cT (fin_ xclass) cT.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass cT.
+Definition finZmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @GRing.Ring.Pack cT xclass xT.
+Definition join_finType := @Finite.Pack ringType (fin_ xclass) xT.
+Definition join_finZmodType := @Zmodule.Pack ringType xclass xT.
Definition baseFinGroupType := base_group cT zmodType finType.
Definition finGroupType := fin_group baseFinGroupType zmodType.
@@ -267,19 +271,21 @@ Local Coercion sort : type >-> Sortclass.
Definition pack := gen_pack Pack Class GRing.ComRing.class.
Variable cT : type.
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition countType := Countable.Pack (fin_ class) cT.
-Definition finType := Finite.Pack (fin_ class) cT.
-Definition zmodType := GRing.Zmodule.Pack class cT.
-Definition finZmodType := Zmodule.Pack class cT.
-Definition ringType := GRing.Ring.Pack class cT.
-Definition finRingType := Ring.Pack class cT.
-Definition comRingType := GRing.ComRing.Pack class cT.
-Definition join_finType := @Finite.Pack comRingType (fin_ class) cT.
-Definition join_finZmodType := @Zmodule.Pack comRingType class cT.
-Definition join_finRingType := @Ring.Pack comRingType class cT.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition countType := @Countable.Pack cT (fin_ xclass) xT.
+Definition finType := @Finite.Pack cT (fin_ xclass) xT.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
+Definition finZmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @GRing.Ring.Pack cT xclass xT.
+Definition finRingType := @Ring.Pack cT xclass xT.
+Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
+Definition join_finType := @Finite.Pack comRingType (fin_ xclass) xT.
+Definition join_finZmodType := @Zmodule.Pack comRingType xclass xT.
+Definition join_finRingType := @Ring.Pack comRingType xclass xT.
Definition baseFinGroupType := base_group cT zmodType finType.
Definition finGroupType := fin_group baseFinGroupType zmodType.
@@ -341,20 +347,22 @@ Local Coercion sort : type >-> Sortclass.
Definition pack := gen_pack Pack Class GRing.UnitRing.class.
Variable cT : type.
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition countType := Countable.Pack (fin_ class) cT.
-Definition finType := Finite.Pack (fin_ class) cT.
-Definition zmodType := GRing.Zmodule.Pack class cT.
-Definition finZmodType := Zmodule.Pack class cT.
-Definition ringType := GRing.Ring.Pack class cT.
-Definition finRingType := Ring.Pack class cT.
-Definition unitRingType := GRing.UnitRing.Pack class cT.
-
-Definition join_finType := @Finite.Pack unitRingType (fin_ class) cT.
-Definition join_finZmodType := @Zmodule.Pack unitRingType class cT.
-Definition join_finRingType := @Ring.Pack unitRingType class cT.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition countType := @Countable.Pack cT (fin_ xclass) xT.
+Definition finType := @Finite.Pack cT (fin_ xclass) xT.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
+Definition finZmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @GRing.Ring.Pack cT xclass xT.
+Definition finRingType := @Ring.Pack cT xclass xT.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
+
+Definition join_finType := @Finite.Pack unitRingType (fin_ xclass) xT.
+Definition join_finZmodType := @Zmodule.Pack unitRingType xclass xT.
+Definition join_finRingType := @Ring.Pack unitRingType xclass xT.
Definition baseFinGroupType := base_group cT zmodType finType.
Definition finGroupType := fin_group baseFinGroupType zmodType.
@@ -498,29 +506,31 @@ Local Coercion sort : type >-> Sortclass.
Definition pack := gen_pack Pack Class GRing.ComUnitRing.class.
Variable cT : type.
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition countType := Countable.Pack (fin_ class) cT.
-Definition finType := Finite.Pack (fin_ class) cT.
-Definition zmodType := GRing.Zmodule.Pack class cT.
-Definition finZmodType := Zmodule.Pack class cT.
-Definition ringType := GRing.Ring.Pack class cT.
-Definition finRingType := Ring.Pack class cT.
-Definition comRingType := GRing.ComRing.Pack class cT.
-Definition finComRingType := ComRing.Pack class cT.
-Definition unitRingType := GRing.UnitRing.Pack class cT.
-Definition finUnitRingType := UnitRing.Pack class cT.
-Definition comUnitRingType := GRing.ComUnitRing.Pack class cT.
-
-Definition join_finType := @Finite.Pack comUnitRingType (fin_ class) cT.
-Definition join_finZmodType := @Zmodule.Pack comUnitRingType class cT.
-Definition join_finRingType := @Ring.Pack comUnitRingType class cT.
-Definition join_finComRingType := @ComRing.Pack comUnitRingType class cT.
-Definition join_finUnitRingType := @UnitRing.Pack comUnitRingType class cT.
-Definition ujoin_finComRingType := @ComRing.Pack unitRingType class cT.
-Definition cjoin_finUnitRingType := @UnitRing.Pack comRingType class cT.
-Definition fcjoin_finUnitRingType := @UnitRing.Pack finComRingType class cT.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition countType := @Countable.Pack cT (fin_ xclass) xT.
+Definition finType := @Finite.Pack cT (fin_ xclass) xT.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
+Definition finZmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @GRing.Ring.Pack cT xclass xT.
+Definition finRingType := @Ring.Pack cT xclass xT.
+Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
+Definition finComRingType := @ComRing.Pack cT xclass xT.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
+Definition finUnitRingType := @UnitRing.Pack cT xclass xT.
+Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
+
+Definition join_finType := @Finite.Pack comUnitRingType (fin_ xclass) xT.
+Definition join_finZmodType := @Zmodule.Pack comUnitRingType xclass xT.
+Definition join_finRingType := @Ring.Pack comUnitRingType xclass xT.
+Definition join_finComRingType := @ComRing.Pack comUnitRingType xclass xT.
+Definition join_finUnitRingType := @UnitRing.Pack comUnitRingType xclass xT.
+Definition ujoin_finComRingType := @ComRing.Pack unitRingType xclass xT.
+Definition cjoin_finUnitRingType := @UnitRing.Pack comRingType xclass xT.
+Definition fcjoin_finUnitRingType := @UnitRing.Pack finComRingType xclass xT.
Definition baseFinGroupType := base_group cT zmodType finType.
Definition finGroupType := fin_group baseFinGroupType zmodType.
@@ -596,29 +606,31 @@ Local Coercion sort : type >-> Sortclass.
Definition pack := gen_pack Pack Class GRing.IntegralDomain.class.
Variable cT : type.
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition countType := Countable.Pack (fin_ class) cT.
-Definition finType := Finite.Pack (fin_ class) cT.
-Definition zmodType := GRing.Zmodule.Pack class cT.
-Definition finZmodType := Zmodule.Pack class cT.
-Definition ringType := GRing.Ring.Pack class cT.
-Definition finRingType := Ring.Pack class cT.
-Definition comRingType := GRing.ComRing.Pack class cT.
-Definition finComRingType := ComRing.Pack class cT.
-Definition unitRingType := GRing.UnitRing.Pack class cT.
-Definition finUnitRingType := UnitRing.Pack class cT.
-Definition comUnitRingType := GRing.ComUnitRing.Pack class cT.
-Definition finComUnitRingType := ComUnitRing.Pack class cT.
-Definition idomainType := GRing.IntegralDomain.Pack class cT.
-
-Definition join_finType := @Finite.Pack idomainType (fin_ class) cT.
-Definition join_finZmodType := @Zmodule.Pack idomainType class cT.
-Definition join_finRingType := @Ring.Pack idomainType class cT.
-Definition join_finUnitRingType := @UnitRing.Pack idomainType class cT.
-Definition join_finComRingType := @ComRing.Pack idomainType class cT.
-Definition join_finComUnitRingType := @ComUnitRing.Pack idomainType class cT.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition countType := @Countable.Pack cT (fin_ xclass) xT.
+Definition finType := @Finite.Pack cT (fin_ xclass) xT.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
+Definition finZmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @GRing.Ring.Pack cT xclass xT.
+Definition finRingType := @Ring.Pack cT xclass xT.
+Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
+Definition finComRingType := @ComRing.Pack cT xclass xT.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
+Definition finUnitRingType := @UnitRing.Pack cT xclass xT.
+Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
+Definition finComUnitRingType := @ComUnitRing.Pack cT xclass xT.
+Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
+
+Definition join_finType := @Finite.Pack idomainType (fin_ xclass) xT.
+Definition join_finZmodType := @Zmodule.Pack idomainType xclass xT.
+Definition join_finRingType := @Ring.Pack idomainType xclass xT.
+Definition join_finUnitRingType := @UnitRing.Pack idomainType xclass xT.
+Definition join_finComRingType := @ComRing.Pack idomainType xclass xT.
+Definition join_finComUnitRingType := @ComUnitRing.Pack idomainType xclass xT.
Definition baseFinGroupType := base_group cT zmodType finType.
Definition finGroupType := fin_group baseFinGroupType zmodType.
@@ -695,32 +707,34 @@ Local Coercion sort : type >-> Sortclass.
Definition pack := gen_pack Pack Class GRing.Field.class.
Variable cT : type.
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition countType := Countable.Pack (fin_ class) cT.
-Definition finType := Finite.Pack (fin_ class) cT.
-Definition zmodType := GRing.Zmodule.Pack class cT.
-Definition finZmodType := Zmodule.Pack class cT.
-Definition ringType := GRing.Ring.Pack class cT.
-Definition finRingType := Ring.Pack class cT.
-Definition comRingType := GRing.ComRing.Pack class cT.
-Definition finComRingType := ComRing.Pack class cT.
-Definition unitRingType := GRing.UnitRing.Pack class cT.
-Definition finUnitRingType := UnitRing.Pack class cT.
-Definition comUnitRingType := GRing.ComUnitRing.Pack class cT.
-Definition finComUnitRingType := ComUnitRing.Pack class cT.
-Definition idomainType := GRing.IntegralDomain.Pack class cT.
-Definition finIdomainType := IntegralDomain.Pack class cT.
-Definition fieldType := GRing.Field.Pack class cT.
-
-Definition join_finType := @Finite.Pack fieldType (fin_ class) cT.
-Definition join_finZmodType := @Zmodule.Pack fieldType class cT.
-Definition join_finRingType := @Ring.Pack fieldType class cT.
-Definition join_finUnitRingType := @UnitRing.Pack fieldType class cT.
-Definition join_finComRingType := @ComRing.Pack fieldType class cT.
-Definition join_finComUnitRingType := @ComUnitRing.Pack fieldType class cT.
-Definition join_finIdomainType := @IntegralDomain.Pack fieldType class cT.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition countType := @Countable.Pack cT (fin_ xclass) xT.
+Definition finType := @Finite.Pack cT (fin_ xclass) xT.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
+Definition finZmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @GRing.Ring.Pack cT xclass xT.
+Definition finRingType := @Ring.Pack cT xclass xT.
+Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
+Definition finComRingType := @ComRing.Pack cT xclass xT.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
+Definition finUnitRingType := @UnitRing.Pack cT xclass xT.
+Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
+Definition finComUnitRingType := @ComUnitRing.Pack cT xclass xT.
+Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
+Definition finIdomainType := @IntegralDomain.Pack cT xclass xT.
+Definition fieldType := @GRing.Field.Pack cT xclass xT.
+
+Definition join_finType := @Finite.Pack fieldType (fin_ xclass) xT.
+Definition join_finZmodType := @Zmodule.Pack fieldType xclass xT.
+Definition join_finRingType := @Ring.Pack fieldType xclass xT.
+Definition join_finUnitRingType := @UnitRing.Pack fieldType xclass xT.
+Definition join_finComRingType := @ComRing.Pack fieldType xclass xT.
+Definition join_finComUnitRingType := @ComUnitRing.Pack fieldType xclass xT.
+Definition join_finIdomainType := @IntegralDomain.Pack fieldType xclass xT.
Definition baseFinGroupType := base_group cT zmodType finType.
Definition finGroupType := fin_group baseFinGroupType zmodType.
@@ -825,16 +839,17 @@ Module DecField.
Section Joins.
Variable cT : Field.type.
-Let class := Field.class cT.
+Let xT := let: Field.Pack T _ _ := cT in T.
+Let xclass : Field.class_of xT := Field.class cT.
Definition type := Eval hnf in DecFieldType cT (DecidableFieldMixin cT).
-Definition finType := @Finite.Pack type (fin_ class) type.
-Definition finZmodType := @Zmodule.Pack type class type.
-Definition finRingType := @Ring.Pack type class type.
-Definition finUnitRingType := @UnitRing.Pack type class type.
-Definition finComRingType := @ComRing.Pack type class type.
-Definition finComUnitRingType := @ComUnitRing.Pack type class type.
-Definition finIdomainType := @IntegralDomain.Pack type class type.
+Definition finType := @Finite.Pack type (fin_ xclass) xT.
+Definition finZmodType := @Zmodule.Pack type xclass xT.
+Definition finRingType := @Ring.Pack type xclass xT.
+Definition finUnitRingType := @UnitRing.Pack type xclass xT.
+Definition finComRingType := @ComRing.Pack type xclass xT.
+Definition finComUnitRingType := @ComUnitRing.Pack type xclass xT.
+Definition finIdomainType := @IntegralDomain.Pack type xclass xT.
Definition baseFinGroupType := base_group type finZmodType finZmodType.
Definition finGroupType := fin_group baseFinGroupType cT.
@@ -873,16 +888,18 @@ Local Coercion sort : type >-> Sortclass.
Variables (phR : phant R) (cT : type phR).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Definition pack := gen_pack (Pack phR) Class (@GRing.Lmodule.class R phR).
-
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition countType := Countable.Pack (fin_ class) cT.
-Definition finType := Finite.Pack (fin_ class) cT.
-Definition zmodType := GRing.Zmodule.Pack class cT.
-Definition finZmodType := Zmodule.Pack class cT.
-Definition lmodType := GRing.Lmodule.Pack phR class cT.
-Definition join_finType := @Finite.Pack lmodType (fin_ class) cT.
-Definition join_finZmodType := @Zmodule.Pack lmodType class cT.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition countType := @Countable.Pack cT (fin_ xclass) xT.
+Definition finType := @Finite.Pack cT (fin_ xclass) xT.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
+Definition finZmodType := @Zmodule.Pack cT xclass xT.
+Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT.
+Definition join_finType := @Finite.Pack lmodType (fin_ xclass) xT.
+Definition join_finZmodType := @Zmodule.Pack lmodType xclass xT.
Definition baseFinGroupType := base_group cT zmodType finType.
Definition finGroupType := fin_group baseFinGroupType zmodType.
@@ -943,26 +960,28 @@ Local Coercion sort : type >-> Sortclass.
Variables (phR : phant R) (cT : type phR).
Definition pack := gen_pack (Pack phR) Class (@GRing.Lalgebra.class R phR).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition countType := Countable.Pack (fin_ class) cT.
-Definition finType := Finite.Pack (fin_ class) cT.
-Definition zmodType := GRing.Zmodule.Pack class cT.
-Definition finZmodType := Zmodule.Pack class cT.
-Definition ringType := GRing.Ring.Pack class cT.
-Definition finRingType := Ring.Pack class cT.
-Definition lmodType := GRing.Lmodule.Pack phR class cT.
-Definition finLmodType := Lmodule.Pack phR class cT.
-Definition lalgType := GRing.Lalgebra.Pack phR class cT.
-
-Definition join_finType := @Finite.Pack lalgType (fin_ class) cT.
-Definition join_finZmodType := @Zmodule.Pack lalgType class cT.
-Definition join_finLmodType := @Lmodule.Pack R phR lalgType class cT.
-Definition join_finRingType := @Ring.Pack lalgType class cT.
-Definition rjoin_finLmodType := @Lmodule.Pack R phR ringType class cT.
-Definition ljoin_finRingType := @Ring.Pack lmodType class cT.
-Definition fljoin_finRingType := @Ring.Pack finLmodType class cT.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition countType := @Countable.Pack cT (fin_ xclass) xT.
+Definition finType := @Finite.Pack cT (fin_ xclass) xT.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
+Definition finZmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @GRing.Ring.Pack cT xclass xT.
+Definition finRingType := @Ring.Pack cT xclass xT.
+Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT.
+Definition finLmodType := @Lmodule.Pack R phR cT xclass xT.
+Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass xT.
+
+Definition join_finType := @Finite.Pack lalgType (fin_ xclass) xT.
+Definition join_finZmodType := @Zmodule.Pack lalgType xclass xT.
+Definition join_finLmodType := @Lmodule.Pack R phR lalgType xclass xT.
+Definition join_finRingType := @Ring.Pack lalgType xclass xT.
+Definition rjoin_finLmodType := @Lmodule.Pack R phR ringType xclass xT.
+Definition ljoin_finRingType := @Ring.Pack lmodType xclass xT.
+Definition fljoin_finRingType := @Ring.Pack finLmodType xclass xT.
Definition baseFinGroupType := base_group cT zmodType finType.
Definition finGroupType := fin_group baseFinGroupType zmodType.
@@ -1035,26 +1054,28 @@ Local Coercion sort : type >-> Sortclass.
Variables (phR : phant R) (cT : type phR).
Definition pack := gen_pack (Pack phR) Class (@GRing.Algebra.class R phR).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition countType := Countable.Pack (fin_ class) cT.
-Definition finType := Finite.Pack (fin_ class) cT.
-Definition zmodType := GRing.Zmodule.Pack class cT.
-Definition finZmodType := Zmodule.Pack class cT.
-Definition ringType := GRing.Ring.Pack class cT.
-Definition finRingType := Ring.Pack class cT.
-Definition lmodType := GRing.Lmodule.Pack phR class cT.
-Definition finLmodType := Lmodule.Pack phR class cT.
-Definition lalgType := GRing.Lalgebra.Pack phR class cT.
-Definition finLalgType := Lalgebra.Pack phR class cT.
-Definition algType := GRing.Algebra.Pack phR class cT.
-
-Definition join_finType := @Finite.Pack algType (fin_ class) cT.
-Definition join_finZmodType := @Zmodule.Pack algType class cT.
-Definition join_finRingType := @Ring.Pack algType class cT.
-Definition join_finLmodType := @Lmodule.Pack R phR algType class cT.
-Definition join_finLalgType := @Lalgebra.Pack R phR algType class cT.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition countType := @Countable.Pack cT (fin_ xclass) xT.
+Definition finType := @Finite.Pack cT (fin_ xclass) xT.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
+Definition finZmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @GRing.Ring.Pack cT xclass xT.
+Definition finRingType := @Ring.Pack cT xclass xT.
+Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT.
+Definition finLmodType := @Lmodule.Pack R phR cT xclass xT.
+Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass xT.
+Definition finLalgType := @Lalgebra.Pack R phR cT xclass xT.
+Definition algType := @GRing.Algebra.Pack R phR cT xclass xT.
+
+Definition join_finType := @Finite.Pack algType (fin_ xclass) xT.
+Definition join_finZmodType := @Zmodule.Pack algType xclass xT.
+Definition join_finRingType := @Ring.Pack algType xclass xT.
+Definition join_finLmodType := @Lmodule.Pack R phR algType xclass xT.
+Definition join_finLalgType := @Lalgebra.Pack R phR algType xclass xT.
Definition baseFinGroupType := base_group cT zmodType finType.
Definition finGroupType := fin_group baseFinGroupType zmodType.
@@ -1130,42 +1151,44 @@ Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variables (phR : phant R) (cT : type phR).
Definition pack := gen_pack (Pack phR) Class (@GRing.UnitAlgebra.class R phR).
-Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
-
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition countType := Countable.Pack (fin_ class) cT.
-Definition finType := Finite.Pack (fin_ class) cT.
-Definition zmodType := GRing.Zmodule.Pack class cT.
-Definition finZmodType := Zmodule.Pack class cT.
-Definition ringType := GRing.Ring.Pack class cT.
-Definition finRingType := Ring.Pack class cT.
-Definition unitRingType := GRing.UnitRing.Pack class cT.
-Definition finUnitRingType := UnitRing.Pack class cT.
-Definition lmodType := GRing.Lmodule.Pack phR class cT.
-Definition finLmodType := Lmodule.Pack phR class cT.
-Definition lalgType := GRing.Lalgebra.Pack phR class cT.
-Definition finLalgType := Lalgebra.Pack phR class cT.
-Definition algType := GRing.Algebra.Pack phR class cT.
-Definition finAlgType := Algebra.Pack phR class cT.
-Definition unitAlgType := GRing.UnitAlgebra.Pack phR class cT.
-
-Definition join_finType := @Finite.Pack unitAlgType (fin_ class) cT.
-Definition join_finZmodType := @Zmodule.Pack unitAlgType class cT.
-Definition join_finRingType := @Ring.Pack unitAlgType class cT.
-Definition join_finUnitRingType := @UnitRing.Pack unitAlgType class cT.
-Definition join_finLmodType := @Lmodule.Pack R phR unitAlgType class cT.
-Definition join_finLalgType := @Lalgebra.Pack R phR unitAlgType class cT.
-Definition join_finAlgType := @Algebra.Pack R phR unitAlgType class cT.
-Definition ljoin_finUnitRingType := @UnitRing.Pack lmodType class cT.
-Definition fljoin_finUnitRingType := @UnitRing.Pack finLmodType class cT.
-Definition njoin_finUnitRingType := @UnitRing.Pack lalgType class cT.
-Definition fnjoin_finUnitRingType := @UnitRing.Pack finLalgType class cT.
-Definition ajoin_finUnitRingType := @UnitRing.Pack algType class cT.
-Definition fajoin_finUnitRingType := @UnitRing.Pack finAlgType class cT.
-Definition ujoin_finLmodType := @Lmodule.Pack R phR unitRingType class cT.
-Definition ujoin_finLalgType := @Lalgebra.Pack R phR unitRingType class cT.
-Definition ujoin_finAlgType := @Algebra.Pack R phR unitRingType class cT.
+Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition countType := @Countable.Pack cT (fin_ xclass) xT.
+Definition finType := @Finite.Pack cT (fin_ xclass) xT.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
+Definition finZmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @GRing.Ring.Pack cT xclass xT.
+Definition finRingType := @Ring.Pack cT xclass xT.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
+Definition finUnitRingType := @UnitRing.Pack cT xclass xT.
+Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT.
+Definition finLmodType := @Lmodule.Pack R phR cT xclass xT.
+Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass xT.
+Definition finLalgType := @Lalgebra.Pack R phR cT xclass xT.
+Definition algType := @GRing.Algebra.Pack R phR cT xclass xT.
+Definition finAlgType := @Algebra.Pack R phR cT xclass xT.
+Definition unitAlgType := @GRing.UnitAlgebra.Pack R phR cT xclass xT.
+
+Definition join_finType := @Finite.Pack unitAlgType (fin_ xclass) xT.
+Definition join_finZmodType := @Zmodule.Pack unitAlgType xclass xT.
+Definition join_finRingType := @Ring.Pack unitAlgType xclass xT.
+Definition join_finUnitRingType := @UnitRing.Pack unitAlgType xclass xT.
+Definition join_finLmodType := @Lmodule.Pack R phR unitAlgType xclass xT.
+Definition join_finLalgType := @Lalgebra.Pack R phR unitAlgType xclass xT.
+Definition join_finAlgType := @Algebra.Pack R phR unitAlgType xclass xT.
+Definition ljoin_finUnitRingType := @UnitRing.Pack lmodType xclass xT.
+Definition fljoin_finUnitRingType := @UnitRing.Pack finLmodType xclass xT.
+Definition njoin_finUnitRingType := @UnitRing.Pack lalgType xclass xT.
+Definition fnjoin_finUnitRingType := @UnitRing.Pack finLalgType xclass xT.
+Definition ajoin_finUnitRingType := @UnitRing.Pack algType xclass xT.
+Definition fajoin_finUnitRingType := @UnitRing.Pack finAlgType xclass xT.
+Definition ujoin_finLmodType := @Lmodule.Pack R phR unitRingType xclass xT.
+Definition ujoin_finLalgType := @Lalgebra.Pack R phR unitRingType xclass xT.
+Definition ujoin_finAlgType := @Algebra.Pack R phR unitRingType xclass xT.
Definition baseFinGroupType := base_group cT zmodType finType.
Definition finGroupType := fin_group baseFinGroupType zmodType.
diff --git a/fingroup.v b/fingroup.v
index 13110742..09f47a87 100644
--- a/fingroup.v
+++ b/fingroup.v
@@ -1925,12 +1925,12 @@ Notation "\prod_ ( i \in A | P ) F" :=
Notation "\prod_ ( i \in A ) F" :=
(\big[joinG/1%G]_(i \in A) F%G) : Group_scope.
-Section LaGrange.
+Section Lagrange.
Variable gT : finGroupType.
Implicit Types G H K : {group gT}.
-Lemma LaGrangeI G H : (#|G :&: H| * #|G : H|)%N = #|G|.
+Lemma LagrangeI G H : (#|G :&: H| * #|G : H|)%N = #|G|.
Proof.
rewrite -[#|G|]sum1_card (partition_big_imset (rcoset H)) /=.
rewrite mulnC -sum_nat_const; apply: eq_bigr => _ /rcosetsP[x Gx ->].
@@ -1940,19 +1940,19 @@ by rewrite group_modr sub1set // inE.
Qed.
Lemma divgI G H : #|G| %/ #|G :&: H| = #|G : H|.
-Proof. by rewrite -(LaGrangeI G H) mulKn ?cardG_gt0. Qed.
+Proof. by rewrite -(LagrangeI G H) mulKn ?cardG_gt0. Qed.
Lemma divg_index G H : #|G| %/ #|G : H| = #|G :&: H|.
-Proof. by rewrite -(LaGrangeI G H) mulnK. Qed.
+Proof. by rewrite -(LagrangeI G H) mulnK. Qed.
Lemma dvdn_indexg G H : #|G : H| %| #|G|.
-Proof. by rewrite -(LaGrangeI G H) dvdn_mull. Qed.
+Proof. by rewrite -(LagrangeI G H) dvdn_mull. Qed.
-Theorem LaGrange G H : H \subset G -> (#|H| * #|G : H|)%N = #|G|.
-Proof. by move/setIidPr=> sHG; rewrite -{1}sHG LaGrangeI. Qed.
+Theorem Lagrange G H : H \subset G -> (#|H| * #|G : H|)%N = #|G|.
+Proof. by move/setIidPr=> sHG; rewrite -{1}sHG LagrangeI. Qed.
Lemma cardSg G H : H \subset G -> #|H| %| #|G|.
-Proof. by move/LaGrange <-; rewrite dvdn_mulr. Qed.
+Proof. by move/Lagrange <-; rewrite dvdn_mulr. Qed.
Lemma lognSg p G H : G \subset H -> logn p #|G| <= logn p #|H|.
Proof. by move=> sGH; rewrite dvdn_leq_log ?cardSg. Qed.
@@ -1964,7 +1964,7 @@ exact: dvdn_trans (cardSg sGH).
Qed.
Lemma divgS G H : H \subset G -> #|G| %/ #|H| = #|G : H|.
-Proof. by move/LaGrange <-; rewrite mulKn. Qed.
+Proof. by move/Lagrange <-; rewrite mulKn. Qed.
Lemma coprimeSg G H p : H \subset G -> coprime #|G| p -> coprime #|H| p.
Proof. by move=> sHG; exact: coprime_dvdl (cardSg sHG). Qed.
@@ -1984,11 +1984,11 @@ apply/esym/eqP; rewrite eqEcard sub1set [#|_|]indexgg cards1 andbT.
by apply/rcosetsP; exists 1; rewrite ?mulg1.
Qed.
-Lemma LaGrange_index G H K :
+Lemma Lagrange_index G H K :
H \subset G -> K \subset H -> (#|G : H| * #|H : K|)%N = #|G : K|.
Proof.
move=> sHG sKH; apply/eqP; rewrite mulnC -(eqn_pmul2l (cardG_gt0 K)).
-by rewrite mulnA !LaGrange // (subset_trans sKH).
+by rewrite mulnA !Lagrange // (subset_trans sKH).
Qed.
Lemma indexgI G H : #|G : G :&: H| = #|G : H|.
@@ -1996,19 +1996,19 @@ Proof. by rewrite -divgI divgS ?subsetIl. Qed.
Lemma indexgS G H K : H \subset K -> #|G : K| %| #|G : H|.
Proof.
-move=> sHK; rewrite -(@dvdn_pmul2l #|G :&: K|) ?cardG_gt0 // LaGrangeI.
-by rewrite -(LaGrange (setIS G sHK)) mulnAC LaGrangeI dvdn_mulr.
+move=> sHK; rewrite -(@dvdn_pmul2l #|G :&: K|) ?cardG_gt0 // LagrangeI.
+by rewrite -(Lagrange (setIS G sHK)) mulnAC LagrangeI dvdn_mulr.
Qed.
Lemma indexSg G H K : H \subset K -> K \subset G -> #|K : H| %| #|G : H|.
Proof.
move=> sHK sKG; rewrite -(@dvdn_pmul2l #|H|) ?cardG_gt0 //.
-by rewrite !LaGrange ?(cardSg, subset_trans sHK).
+by rewrite !Lagrange ?(cardSg, subset_trans sHK).
Qed.
Lemma indexg_eq1 G H : (#|G : H| == 1%N) = (G \subset H).
Proof.
-rewrite eqn_leq -(leq_pmul2l (cardG_gt0 (G :&: H))) LaGrangeI muln1.
+rewrite eqn_leq -(leq_pmul2l (cardG_gt0 (G :&: H))) LagrangeI muln1.
by rewrite indexg_gt0 andbT (sameP setIidPl eqP) eqEcard subsetIl.
Qed.
@@ -2044,17 +2044,17 @@ Qed.
Lemma rcosets_partition G H : H \subset G -> partition (rcosets H G) G.
Proof. by move/mulSGid=> {2}<-; exact: rcosets_partition_mul. Qed.
-Lemma LaGrangeMl G H : (#|G| * #|H : G|)%N = #|G * H|.
+Lemma LagrangeMl G H : (#|G| * #|H : G|)%N = #|G * H|.
Proof.
rewrite mulnC -(card_uniform_partition _ (rcosets_partition_mul H G)) //.
by move=> _ /rcosetsP[x Hx ->]; rewrite card_rcoset.
Qed.
-Lemma LaGrangeMr G H : (#|G : H| * #|H|)%N = #|G * H|.
-Proof. by rewrite mulnC LaGrangeMl -card_invg invMg !invGid. Qed.
+Lemma LagrangeMr G H : (#|G : H| * #|H|)%N = #|G * H|.
+Proof. by rewrite mulnC LagrangeMl -card_invg invMg !invGid. Qed.
Lemma mul_cardG G H : (#|G| * #|H| = #|G * H|%g * #|G :&: H|)%N.
-Proof. by rewrite -LaGrangeMr -(LaGrangeI G H) -mulnA mulnC. Qed.
+Proof. by rewrite -LagrangeMr -(LagrangeI G H) -mulnA mulnC. Qed.
Lemma dvdn_cardMg G H : #|G * H| %| #|G| * #|H|.
Proof. by rewrite mul_cardG dvdn_mulr. Qed.
@@ -2099,12 +2099,12 @@ Lemma coprime_index_mulG G H K :
Proof.
move=> sHG sKG co_iG_HK; apply/eqP; rewrite eqEcard mul_subG //=.
rewrite -(@leq_pmul2r #|H :&: K|) ?cardG_gt0 // -mul_cardG.
-rewrite -(LaGrange sHG) -(LaGrangeI K H) mulnAC setIC -mulnA.
+rewrite -(Lagrange sHG) -(LagrangeI K H) mulnAC setIC -mulnA.
rewrite !leq_pmul2l ?cardG_gt0 // dvdn_leq // -(Gauss_dvdr _ co_iG_HK).
-by rewrite -(indexgI K) LaGrange_index ?indexgS ?subsetIl ?subsetIr.
+by rewrite -(indexgI K) Lagrange_index ?indexgS ?subsetIl ?subsetIr.
Qed.
-End LaGrange.
+End Lagrange.
Section GeneratedGroup.
@@ -2768,7 +2768,7 @@ Lemma rcoset_index2 G H x :
H \subset G -> #|G : H| = 2 -> x \in G :\: H -> H :* x = G :\: H.
Proof.
move=> sHG indexHG => /setDP[Gx notHx]; apply/eqP.
-rewrite eqEcard -(leq_add2l #|G :&: H|) cardsID -(LaGrangeI G H) indexHG muln2.
+rewrite eqEcard -(leq_add2l #|G :&: H|) cardsID -(LagrangeI G H) indexHG muln2.
rewrite (setIidPr sHG) card_rcoset addnn leqnn andbT.
apply/subsetP=> _ /rcosetP[y Hy ->]; apply/setDP.
by rewrite !groupMl // (subsetP sHG).
diff --git a/fintype.v b/fintype.v
index c9e5b291..0819721e 100644
--- a/fintype.v
+++ b/fintype.v
@@ -186,14 +186,16 @@ Local Coercion sort : type >-> Sortclass.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c T.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
Definition pack b0 (m0 : mixin_of (EqType T b0)) :=
fun bT b & phant_id (Choice.class bT) b =>
fun m & phant_id m0 m => Pack (@Class T b m) T.
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition countType := Countable.Pack (base2 class) cT.
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition countType := @Countable.Pack cT (base2 xclass) xT.
End ClassDef.
diff --git a/frobenius.v b/frobenius.v
index cd8d6343..37443c58 100644
--- a/frobenius.v
+++ b/frobenius.v
@@ -682,9 +682,9 @@ pose G' := ('C_G[y] / <[y]>)%G; pose n' := gcdn #|G'| n`_p^'.
have n'_gt0: 0 < n' by rewrite gcdn_gt0 cardG_gt0.
rewrite (eq_bigr (fun _ => #|'Ldiv_n'(G')|)) => [|_ /imsetP[a Ga ->]].
rewrite sum_nat_const -index_cent1 indexgI.
- rewrite -(dvdn_pmul2l (cardG_gt0 'C_G[y])) mulnA LaGrangeI.
+ rewrite -(dvdn_pmul2l (cardG_gt0 'C_G[y])) mulnA LagrangeI.
have oCy: #|'C_G[y]| = (#[y] * #|G'|)%N.
- rewrite card_quotient ?subcent1_cycle_norm // LaGrange //.
+ rewrite card_quotient ?subcent1_cycle_norm // Lagrange //.
by rewrite subcent1_cycle_sub ?groupX.
rewrite oCy -mulnA -(muln_lcm_gcd #|G'|) -/n' mulnA dvdn_mul //.
rewrite muln_lcmr -oCy order_constt pA // mulnAC partnC // dvdn_lcm.
@@ -710,7 +710,7 @@ apply: eq_bigl => z; apply/andP/andP=> [[]|[]].
have G'z: h z \in G' by rewrite mem_morphim //= inE groupJ // groupV.
rewrite inE G'z inE -order_dvdn dvdn_gcd order_dvdG //=.
rewrite /order -morphim_cycle // -quotientE card_quotient ?cycle_subG //.
- rewrite -(@dvdn_pmul2l #[y]) // LaGrange; last first.
+ rewrite -(@dvdn_pmul2l #[y]) // Lagrange; last first.
by rewrite /= cycleJ cycle_subG mem_conjgV -zp_ya mem_cycle.
rewrite oy mulnAC partnC // [#|_|]orderJ; split.
by rewrite !inE -!order_dvdn mulnC in Az; case/andP: Az.
@@ -740,7 +740,7 @@ rewrite -(conjgKV a z) !inE groupJ //= -!order_dvdn orderJ; apply/andP; split.
rewrite -(partnC p n_gt0) mulnCA mulnA -oy -(@partnC p #[_]) // ozp.
apply dvdn_mul => //; apply: dvdn_trans (dvdn_trans n'Z (dvdn_gcdr _ _)).
rewrite {2}/order -morphim_cycle // -quotientE card_quotient ?cycle_subG //.
-rewrite -(@dvdn_pmul2l #|<[z ^ a^-1]> :&: <[y]>|) ?cardG_gt0 // LaGrangeI.
+rewrite -(@dvdn_pmul2l #|<[z ^ a^-1]> :&: <[y]>|) ?cardG_gt0 // LagrangeI.
rewrite -[#|<[_]>|](partnC p) ?order_gt0 // dvdn_pmul2r // ozp.
by rewrite cardSg ?subsetIr.
Qed.
diff --git a/galgebra.v b/galgebra.v
index 95d9d704..e79c65a1 100644
--- a/galgebra.v
+++ b/galgebra.v
@@ -188,10 +188,14 @@ exists (fun x : 'rV[F]_#|gT| => GAlg ([ffun k => (x 0 (enum_rank k))])) => x.
by apply/rowP=> i; rewrite // !mxE galgE enum_valK.
Qed.
-Definition gAlgMixin := VectMixin gAlg_iso_vect.
-Canonical gAlgVectType := VectType F galg gAlgMixin.
+Definition galg_vectMixin := VectMixin gAlg_iso_vect.
+Canonical galg_vectType := VectType F galg galg_vectMixin.
+
+Canonical galg_unitRingType := FalgUnitRingType galg.
+Canonical galg_unitAlgFType := [unitAlgType F of galg].
Canonical gAlgAlgFType := [FalgType F of galg].
+
Variable G : {group gT}.
Definition gvspace: {vspace galg} := (\sum_(g \in G) <[g%:FG]>)%VS.
diff --git a/galois.v b/galois.v
index d558d9c0..90c61acd 100644
--- a/galois.v
+++ b/galois.v
@@ -129,7 +129,7 @@ Variables (K E: {vspace L}).
(* Should I make this canonical by setting fixing (f @: E)^C ? *)
Definition kHom : pred 'End(L) :=
-fun f => (K <= eigenspace f 1)%VS &&
+ fun f => (K <= eigenspace f 1)%VS &&
(all (fun v1 => all (fun v2 => f (v1 * v2) == f v1 * f v2) (vbasis E))
(vbasis E)).
@@ -174,7 +174,7 @@ case/kHomP => HK _ /polyOverP Hp.
by apply/polyP => i; rewrite coef_map /= HK ?Hp.
Qed.
-Definition kAut : pred 'End(L) := fun f => kHom f && (f @: E == E)%VS.
+Definition kAut : pred 'End(L) := fun f => kHom f && (f @: E == E)%VS.
Fact kHomExtendF_subproof x y :
linear (fun z => (map_poly f (poly_for_Fadjoin E x z)).[y]).
@@ -258,24 +258,24 @@ split; first by move => a b; rewrite /= HE // subvsP.
by rewrite /= algid1 HK // mem1v.
Qed.
-Lemma kHom_root : forall p x, p \is a polyOver E -> x \in E ->
- root p x -> root (map_poly f p) (f x).
+Lemma kHom_horner p x :
+ p \is a polyOver E -> x \in E -> f p.[x] = (map_poly f p).[f x].
Proof.
-rewrite/root.
-move => ? x.
-case/polyOver_subvs => p -> Hx.
-set (f' := (RMorphism kHomRmorph_subproof)).
-rewrite -[x]/(vsval (Subvs Hx)) -map_poly_comp ?linear0 //.
-rewrite (horner_map f') horner_map.
-move/eqP => /= ->.
-by rewrite linear0.
+case/polyOver_subvs=> {p}p -> Ex; rewrite (horner_map _ _ (Subvs Ex)).
+by rewrite -[f _](horner_map (RMorphism kHomRmorph_subproof)) map_poly_comp.
Qed.
-Lemma kHom_rootK : forall p x, p \is a polyOver K -> x \in E ->
- root p x -> root p (f x).
+Lemma kHom_root p x :
+ p \is a polyOver E -> x \in E -> root p x -> root (map_poly f p) (f x).
Proof.
-move => p x Hp Hx Hroot.
-by rewrite -(kHomFixedPoly Hf Hp) kHom_root // (polyOverSv HKE).
+by move=> Ep Ex /rootP px0; rewrite /root -kHom_horner // px0 linear0.
+Qed.
+
+Lemma kHom_rootK p x :
+ p \is a polyOver K -> x \in E -> root p x -> root p (f x).
+Proof.
+move=> Kp Ex /kHom_root; rewrite (kHomFixedPoly Hf) //.
+by apply; rewrite ?(polyOverSv HKE).
Qed.
Variables (x y : L).
@@ -486,61 +486,13 @@ rewrite -[fj _](horner_map (RMorphism fjM)) (kHomFixedPoly homLfj) //.
by rewrite /= lfunE /= Dfz -fi_z lker0_lfunK.
Qed.
-(* To prove this hypothesis it is suffices to prove NormalFieldExt F.
- Actually, it suffices to prove
- (forall x, x \in basis -> NormalFieldExt F x)
- for some basis of L.
- The proof that this suffices should eventually be done. *)
+(* The lemma for discharging this assumption for splitting fields is in a *)
+(* separate section because its proof needs to apply kHom_extends to a larger *)
+(* extension field. *)
Definition isNormalFieldExt :=
forall K x, exists r, minPoly K x == \prod_(y <- r) ('X - y%:P).
-Lemma splitting_field_normal p :
- p \is a polyOver 1%VS -> splittingFieldFor 1%VS p fullv ->
- separablePolynomial p ->
- isNormalFieldExt.
-Proof.
-move=> F0p splitLp sep_p K x; set pKx := minPoly K x.
-have [autL /(_ sep_p)UautL DautL] := enum_kHom F0p splitLp.
-pose q := \prod_(z <- [image tnth autL i x | i <- 'I__]) ('X - z%:P).
-suffices F0q: q \is a polyOver 1%VS.
- suffices /dvdp_prod_XsubC[m]: pKx %| q.
- move: (mask m _) => r; exists r.
- by rewrite -eqpMP ?monic_prod_XsubC ?monic_minPoly.
- rewrite minPoly_dvdp ?(polyOverSv (sub1v K)) // root_prod_XsubC.
- have /tnthP[i def1]: \1%VF \in autL by rewrite -DautL kHom1.
- by apply/imageP; exists i; rewrite // -def1 id_lfunE.
-have fixed_q f: f \in autL -> map_poly f q = q.
- rewrite -DautL => aut_f.
- have [/LAut_lrmorph fM kerf0] := (aut_f, kAut_lker0 aut_f).
- rewrite /q big_map -filter_index_enum big_filter /=.
- rewrite (rmorph_prod (map_poly_rmorphism (RMorphism fM))).
- have hfP g i: kHom 1 fullv g -> (g \o tnth autL i)%VF \in autL.
- by rewrite -DautL => /comp_kAut->; rewrite ?DautL ?mem_tnth.
- pose hf i := sval (sig_eqW (tnthP _ _ (hfP _ i _))).
- have inj_hf: injective (hf f aut_f).
- apply: can_inj (hf _ (inv_kAut aut_f)) _ => i.
- rewrite {1}/hf; case: (sig_eqW _) => /= k /eqP.
- rewrite /hf; case: (sig_eqW _) => /= _ <-; rewrite lker0_compKf //.
- by rewrite !(tnth_nth 0) nth_uniq ?size_tuple // => /eqP/val_inj.
- rewrite [rhs in _ = rhs](reindex_inj inj_hf); apply: eq_bigr => i _.
- rewrite [RMorphism _]lock rmorphB /= map_polyX map_polyC -lock.
- by rewrite /hf; case: (sig_eqW _) => /= _ <-; rewrite lfunE.
-apply/(all_nthP 0)=> i _ /=; rewrite elemDeg1 eqn_leq andbT.
-rewrite -(@leq_pmul2l (\dim {:L})) -?leq_divRL ?adim_gt0 //.
-rewrite muln1 -[elementDegree _ _]mul1n -{1}[\dim {:L}]divn1.
-rewrite -(dimv1 L) -dim_Fadjoin -(size_tuple autL).
-set E := Fadjoin _ _; have s1E: (1 <= E)%VS := sub1v _.
-have Ep := polyOverSv s1E F0p.
-have splitEp := splittingFieldForS s1E splitLp.
-have [autE _ DautE] := enum_kHom Ep splitEp; rewrite /= -/E in autE DautE.
-rewrite -(size_tuple autE) uniq_leq_size // => f autLf; rewrite -DautE.
-have hom_f: kHom 1 fullv f by rewrite DautL.
-apply/kHomP; split=> [_ /poly_Fadjoin[t [F0t ->]]|]; last by case/kHomP: hom_f.
-have /LAut_lrmorph fM := hom_f; rewrite -[f _](horner_map (RMorphism fM)).
-by rewrite (kHomFixedPoly hom_f) // -coef_map fixed_q.
-Qed.
-
Hypothesis NormalFieldExt : isNormalFieldExt.
Lemma normal_field_splitting :
@@ -2499,12 +2451,131 @@ Section UseGalois.
Variables (F0 : fieldType) (L : fieldExtType F0).
+Lemma splitting_field_normal p :
+ p \is a polyOver 1%VS -> splittingFieldFor 1 p {:L} -> isNormalFieldExt L.
+Proof.
+move=> F0p splitLp K x; pose q1 := minPoly 1 x.
+have [autL _ DautL] := enum_kHom F0p splitLp.
+suffices{K} autL_px q:
+ q %| q1 -> size q > 1 -> has (fun f : 'End(L) => root q (f x)) autL.
+- set q := minPoly K x; have: q \is monic by exact: monic_minPoly.
+ have: q %| q1.
+ by rewrite minPoly_dvdp ?root_minPoly ?(polyOverSv (sub1v K)) ?minPolyOver.
+ elim: {q}_.+1 {-2}q (ltnSn (size q)) => // d IHd q leqd q_dv_q1.
+ move=> mon_q; have [/size1_polyC Dq | q_gt1] := leqP (size q) 1.
+ exists nil; rewrite big_nil Dq (inj_eq (@polyC_inj _)).
+ by rewrite qualifE Dq lead_coefC in mon_q.
+ have /hasP[f autLf /factor_theorem[q2 Dq]] := autL_px q q_dv_q1 q_gt1.
+ have mon_q2: q2 \is monic by rewrite -(monicMr _ (monicXsubC (f x))) -Dq.
+ rewrite Dq size_monicM -?size_poly_eq0 ?size_XsubC ?addn2 //= in leqd.
+ have q2_dv_q1: q2 %| q1 by rewrite (dvdp_trans _ q_dv_q1) // Dq dvdp_mulr.
+ rewrite Dq; have [r /eqP->] := IHd q2 leqd q2_dv_q1 mon_q2.
+ by exists (f x :: r); rewrite big_cons mulrC.
+elim: {q}_.+1 {-2}q (ltnSn (size q)) => // d IHd q leqd q_dv_q1 q_gt1.
+without loss{d leqd IHd q_gt1} irr_q: q q_dv_q1 / irreducible_poly q.
+ move=> IHq; apply: wlog_neg => not_autLx_q; apply: IHq => //.
+ split=> // q2 q2_dv_q; apply: contraR not_autLx_q => /norP[q2_neq1 ltq2q].
+ have{q2_neq1} q2_gt1: size q2 > 1.
+ rewrite ltn_neqAle eq_sym size_poly_eq1 q2_neq1 size_poly_gt0.
+ apply: contraTneq q_gt1 => q2_0; rewrite -(divpK q2_dv_q) q2_0 mulr0.
+ by rewrite size_poly0.
+ have ltq2d: size q2 < d.
+ rewrite -ltnS (leq_trans _ leqd) // ltnS ltn_neqAle dvdp_size_eqp //.
+ by rewrite ltq2q dvdp_leq // -size_poly_eq0 -(subnKC q_gt1).
+ apply: sub_has (IHd _ ltq2d (dvdp_trans q2_dv_q q_dv_q1) q2_gt1) => f.
+ by rewrite !root_factor_theorem => /dvdp_trans->.
+have{irr_q} [Lz [inLz [z qz0]]]: {Lz : fieldExtType F0 &
+ {inLz : {lrmorphism L -> Lz} & {z : Lz | root (map_poly inLz q) z}}}.
+- have [Lz0 _ [z qz0 defLz]] := irredp_FAdjoin irr_q.
+ pose Lz := baseField_extFieldType Lz0.
+ pose inLz : {rmorphism L -> Lz} := [rmorphism of in_alg Lz0].
+ suffices inLzZ: scalable inLz by exists Lz, (AddLRMorphism inLzZ), z.
+ move=> a u; rewrite -{1}mulr_algl rmorphM /=.
+ by rewrite -{1}baseField_scaleE mulr_algl.
+have imL1: (linfun inLz @: 1 = 1)%VS by rewrite limg_line lfunE rmorph1.
+have imLaspace: is_aspace (limg (linfun inLz)).
+ rewrite /is_aspace has_algid1; last by rewrite memvE -imL1 limgS ?sub1v.
+ apply/prodvP=> _ _ /memv_imgP[y1 _ ->] /memv_imgP[y2 _ ->].
+ by rewrite !{1}lfunE -rmorphM -lfunE memv_img ?memvf.
+pose imL := ASpace imLaspace; pose pz := map_poly inLz p.
+have imLin u: inLz u \in imL by rewrite -lfunE memv_img ?memvf.
+have F0pz: pz \is a polyOver 1%VS.
+ apply/polyOverP=> i; rewrite -imL1 coef_map /= -lfunE memv_img //.
+ exact: (polyOverP F0p).
+have{splitLp} splitLpz: splittingFieldFor 1 pz imL.
+ have [r def_p defL] := splitLp; exists (map inLz r).
+ move: def_p; rewrite -(eqp_map inLz) rmorph_prod big_map; congr (_ %= _).
+ by apply: eq_big => // y _; rewrite rmorphB /= map_polyX map_polyC.
+ apply/eqP; rewrite eqEsubv; apply/andP; split.
+ by apply/genFieldP; rewrite sub1v; split=> // _ /mapP[y r_y ->].
+ rewrite /= -{def_p}defL.
+ elim/last_ind: r => [|r y IHr] /=; first by rewrite imL1.
+ rewrite map_rcons !genField_rcons /=.
+ apply/subvP=> _ /memv_imgP[_ /poly_Fadjoin[p1 [r_p1 ->]] ->].
+ rewrite lfunE -horner_map /= mempx_Fadjoin //=; apply/polyOverP=> i.
+ by rewrite coef_map (subvP IHr) //= -lfunE memv_img ?(polyOverP r_p1).
+have [f homLf fxz]: exists2 f : 'End(Lz), kHom 1 imL f & f (inLz x) = z.
+ pose q1z := minPoly 1 (inLz x).
+ have Dq1z: map_poly inLz q1 %| q1z.
+ have F0q1z i: exists a, q1z`_i = a%:A by exact/vlineP/polyOverP/minPolyOver.
+ have [q2 Dq2]: exists q2, q1z = map_poly inLz q2.
+ exists (\poly_(i < size q1z) (sval (sig_eqW (F0q1z i)))%:A).
+ rewrite -{1}[q1z]coefK; apply/polyP=> i; rewrite coef_map !{1}coef_poly.
+ by case: sig_eqW => a; case: ifP; rewrite /= ?rmorph0 ?linearZ ?rmorph1.
+ rewrite Dq2 dvdp_map minPoly_dvdp //.
+ apply/polyOverP=> i; have[a] := F0q1z i; rewrite -(rmorph1 inLz) -linearZ.
+ by rewrite Dq2 coef_map => /fmorph_inj->; rewrite rpredZ ?mem1v.
+ by rewrite -(fmorph_root inLz) -Dq2 root_minPoly.
+ have q1z_z: root q1z z.
+ rewrite !root_factor_theorem in qz0 *.
+ by apply: dvdp_trans qz0 (dvdp_trans _ Dq1z); rewrite dvdp_map.
+ have map1q1z_z: root (map_poly \1%VF q1z) z.
+ by rewrite map_poly_id => // ? _; rewrite lfunE.
+ pose f0 := kHomExtend 1 \1 (inLz x) z.
+ have{map1q1z_z} hom_f0 : kHom 1 (Fadjoin 1 (inLz x)) f0.
+ by apply: kHomExtendkHom map1q1z_z => //; apply: kHom1.
+ have{splitLpz} splitLpz: splittingFieldFor (Fadjoin 1 (inLz x)) pz imL.
+ have [r def_pz defLz] := splitLpz; exists r => //.
+ apply/eqP; rewrite eqEsubv -{2}defLz genFieldSl ?sub1v // andbT.
+ apply/genFieldP; split; last by rewrite -defLz; apply: mem_genField.
+ by rewrite -subsetFadjoinE sub1v -lfunE memv_img ?memvf.
+ have [f homLzf Df] := kHom_extends (sub1v _) hom_f0 F0pz splitLpz.
+ have [-> | x'z] := eqVneq (inLz x) z.
+ by exists \1%VF; rewrite ?lfunE ?kHom1.
+ exists f => //; rewrite -Df ?memx_Fadjoin ?(kHomExtendX _ (kHom1 1 1)) //.
+ apply: contra x'z; rewrite elemDeg1 -eqSS -size_minPoly -/q1z => sz_q1z.
+ have{Dq1z} Dq1z: q1z %= 'X - (inLz x)%:P.
+ rewrite eqp_sym -dvdp_size_eqp ?size_XsubC 1?eq_sym //.
+ by rewrite dvdp_XsubCl root_minPoly.
+ by rewrite (eqp_root Dq1z) root_XsubC eq_sym in q1z_z.
+pose f1 := ((linfun inLz)^-1 \o f \o linfun inLz)%VF.
+have /kHomP[f1id fM] := homLf.
+have Df1 u: inLz (f1 u) = f (inLz u).
+ rewrite !lfunE /= !lfunE /= -lfunE limg_lfunVK //= -[limg _]/(asval imL).
+ have [r def_pz defLz] := splitLpz.
+ have []: all (mem r) r /\ inLz u \in imL by split; first exact/allP.
+ rewrite -{1}defLz; elim/last_ind: {-1}r {u}(inLz u) => [|r1 y IHr1] u.
+ by move=> _ F0u; rewrite f1id // (subvP (sub1v _)).
+ rewrite all_rcons genField_rcons => /andP[rr1 ry] /poly_Fadjoin[pu [r1pu ->]].
+ rewrite (kHom_horner homLf) -defLz; last exact: mem_genField; last first.
+ by apply: polyOverS r1pu; apply/subvP/genFieldSr/allP.
+ apply: rpred_horner.
+ by apply/polyOverP=> i; rewrite coef_map /= defLz IHr1 ?(polyOverP r1pu).
+ rewrite mem_genField // -root_prod_XsubC -(eqp_root def_pz).
+ rewrite (kHom_rootK homLf) ?sub1v //; first by rewrite -defLz mem_genField.
+ by rewrite (eqp_root def_pz) root_prod_XsubC.
+apply/hasP; exists f1; last by rewrite -(fmorph_root inLz) /= Df1 fxz.
+rewrite -DautL; apply/kHomP; split=> [_ /vlineP[a ->] | u v _ _].
+ by apply: (fmorph_inj inLz); rewrite /= Df1 !linearZ rmorph1 /= f1id ?mem1v.
+by apply: (fmorph_inj inLz); rewrite rmorphM /= !Df1 rmorphM fM ?imLin.
+Qed.
+
Lemma splitting_field_galois p :
p \is a polyOver 1%VS -> splittingFieldFor 1 p {:L} ->
separablePolynomial p ->
{normL : isNormalFieldExt L & galois normL 1 fullv}.
Proof.
-move=> F0p splitLp sep_p; have nL := splitting_field_normal F0p splitLp sep_p.
+move=> F0p splitLp sep_p; have nL := splitting_field_normal F0p splitLp.
exists nL; apply/and3P; split; first exact: subvf; last first.
apply/normalP=> y _; have [r /eqP->] := nL 1%AS y.
by exists r => //; apply/allP=> cy _; rewrite /= memvf.
diff --git a/hall.v b/hall.v
index 2a812e56..e4df926c 100644
--- a/hall.v
+++ b/hall.v
@@ -73,9 +73,9 @@ have: Kbar \subset Gbar by rewrite -eqHKbar mulG_subr.
case/inv_quotientS=> //= ZK quoZK sZZK sZKG.
have nZZK: Z <| ZK by exact: normalS nZG.
have cardZK: #|ZK| = (#|Z| * #|G : H|)%N.
- rewrite -(LaGrange sZZK); congr (_ * _)%N.
+ rewrite -(Lagrange sZZK); congr (_ * _)%N.
rewrite -card_quotient -?quoZK; last by case/andP: nZZK.
- rewrite -(divgS sHG) -(LaGrange sZG) -(LaGrange sZH) divnMl //.
+ rewrite -(divgS sHG) -(Lagrange sZG) -(Lagrange sZH) divnMl //.
rewrite -!card_quotient ?normal_norm //= -/Gbar -/Hbar.
by rewrite -eqHKbar (TI_cardMg tiHKbar) mulKn.
have: [splits ZK, over Z].
@@ -92,7 +92,7 @@ have tiHK: H :&: K = 1.
apply/splitsP; exists K; rewrite inE tiHK ?eqEcard subxx leqnn /=.
rewrite mul_subG ?(subset_trans sKZK) //= TI_cardMg //.
rewrite -(@mulKn #|K| #|Z|) ?cardG_gt0 // -TI_cardMg // eqZK.
-by rewrite cardZK mulKn ?cardG_gt0 // LaGrange.
+by rewrite cardZK mulKn ?cardG_gt0 // Lagrange.
Qed.
Theorem SchurZassenhaus_trans_sol gT (H K K1 : {group gT}) :
@@ -114,7 +114,7 @@ have [sMG nMG] := andP nsMG; rewrite -defG => sK1G coHK oK1K.
have nMsG (L : {set gT}): L \subset G -> L \subset 'N(M).
by move/subset_trans->.
have [coKM coHMK]: coprime #|M| #|K| /\ coprime #|H / M| #|K|.
- by apply/andP; rewrite -coprime_mull card_quotient ?nMsG ?LaGrange.
+ by apply/andP; rewrite -coprime_mull card_quotient ?nMsG ?Lagrange.
have oKM (K' : {group gT}): K' \subset G -> #|K'| = #|K| -> #|K' / M| = #|K|.
move=> sK'G oK'.
rewrite -quotientMidr -?norm_joinEl ?card_quotient ?nMsG //; last first.
@@ -244,17 +244,17 @@ have{transHb} transH (K : {group gT}):
by rewrite mem_conjg (subsetP sMH) // -mem_conjg (normP Nx).
have{pi'Hb'} pi'H': pi^'.-nat #|G : H|.
move: pi'Hb'; rewrite -!divgS // def_H !card_quotient //.
- by rewrite -(divnMl (cardG_gt0 M)) !LaGrange.
+ by rewrite -(divnMl (cardG_gt0 M)) !Lagrange.
have [pi_p | pi'p] := boolP (p \in pi).
exists H => //; apply/and3P; split=> //; rewrite /pgroup.
- by rewrite -(LaGrange sMH) -card_quotient // pnat_mul -def_H (pi_pnat pM).
+ by rewrite -(Lagrange sMH) -card_quotient // pnat_mul -def_H (pi_pnat pM).
have [ltHG | leGH {n IHn leGn transH}] := ltnP #|H| #|G|.
case: (IHn _ H (leq_trans ltHG leGn)) => [|H1]; first exact: solvableS solG.
case/and3P=> sH1H piH1 pi'H1' transH1.
have sH1G: H1 \subset G by exact: subset_trans sHG.
exists H1 => [|K sKG piK].
apply/and3P; split => //.
- rewrite -divgS // -(LaGrange sHG) -(LaGrange sH1H) -mulnA.
+ rewrite -divgS // -(Lagrange sHG) -(Lagrange sH1H) -mulnA.
by rewrite mulKn // pnat_mul pi'H1'.
case: (transH K sKG piK) => x Gx def_K.
case: (transH1 (K :^ x^-1)%G) => [||y Hy def_K1].
@@ -436,7 +436,7 @@ have coGNA: coprime #|G :&: N| #|A| := coprimeSg (subsetIl _ _) coGA.
case: (SchurZassenhaus_trans_sol solGN nGNA _ coGNA oAxA) => [|y GNy defAx].
have ->: (G :&: N) * A = N.
apply/eqP; rewrite eqEcard -{2}(mulGid N) mulgSS ?subsetIr //=.
- by rewrite coprime_cardMg // -iGN_A LaGrange ?subsetIr.
+ by rewrite coprime_cardMg // -iGN_A Lagrange ?subsetIr.
rewrite sub_conjgV conjIg -normJ subsetI conjGid ?joing_subl //.
by rewrite mem_gen // inE Gx orbT.
case/setIP: GNy => Gy; case/setIP=> _; move/normP=> nHy.
@@ -602,12 +602,12 @@ have nMHM := subset_trans sHMG nMG.
have{sXHq} sXHM: X \subset HM by rewrite -(quotientSGK nMX) -?defHM.
have{pi'Hq' sHGq} pi'HM': pi^'.-nat #|G : HM|.
move: pi'Hq'; rewrite -!divgS // defHM !card_quotient //.
- by rewrite -(divnMl (cardG_gt0 M)) !LaGrange.
+ by rewrite -(divnMl (cardG_gt0 M)) !Lagrange.
have{nHAq} nHMA: A \subset 'N(HM).
by rewrite -(quotientSGK nMA) ?normsG ?quotient_normG -?defHM //; exact/andP.
case/orP: (orbN (p \in pi)) => pi_p.
exists HM; split=> //; apply/and3P; split; rewrite /pgroup //.
- by rewrite -(LaGrange sMHM) pnat_mul -card_quotient // -defHM (pi_pnat pM).
+ by rewrite -(Lagrange sMHM) pnat_mul -card_quotient // -defHM (pi_pnat pM).
case: (ltnP #|HM| #|G|) => [ltHG | leGHM {n IHn leGn}].
case: (IHn _ A HM X (leq_trans ltHG leGn)) => // [||H [hallH nHA sXH]].
- exact: coprimeSg coGA.
@@ -615,7 +615,7 @@ case: (ltnP #|HM| #|G|) => [ltHG | leGHM {n IHn leGn}].
case/and3P: hallH => sHHM piH pi'H'.
have sHG: H \subset G by exact: subset_trans sHMG.
exists H; split=> //; apply/and3P; split=> //.
- rewrite -divgS // -(LaGrange sHMG) -(LaGrange sHHM) -mulnA mulKn //.
+ rewrite -divgS // -(Lagrange sHMG) -(Lagrange sHHM) -mulnA mulKn //.
by rewrite pnat_mul pi'H'.
have{leGHM nHMA sHMG sMHM sXHM pi'HM'} eqHMG: HM = G.
by apply/eqP; rewrite -val_eqE eqEcard sHMG.
diff --git a/integral_char.v b/integral_char.v
index e1186e53..cd2a36e4 100644
--- a/integral_char.v
+++ b/integral_char.v
@@ -793,6 +793,9 @@ have [n [[pz Dpz] [px Dpx]]] := PET_char0 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 & genField 1 s1 = fullv}}}.
@@ -823,7 +826,7 @@ have rz0: root (pQtoC r) z by rewrite dv_r.
have [q qz0 nz_q | QsV] := Wrap (VectMixin (min_subfx_vectAxiom rz0 nz_r _)).
by rewrite dvdp_leq // -dv_r.
pose Qs := [FalgType rat of _ for VectType rat _ QsV].
-exists [fieldExtType rat of _ for Qs], (subfx_inj_rmorphism QtoC_M z r).
+exists [fieldExtType rat of Qs], (subfx_inj_rmorphism QtoC_M z r).
exists (subfx_eval _ z r 'X) => [|x].
by rewrite /= subfx_inj_eval ?map_polyX ?hornerX.
have{x} [p ->] := subfxE x; exists p.
@@ -2339,7 +2342,7 @@ have [j ->]: exists j, 'chi_i = 'Res 'chi[G]_j.
by exists (iinv (all_rH i)); rewrite DrH f_iinv.
apply/subset_cardP; last exact/subsetP; apply/esym/eqP.
rewrite card_Iirr_abelian ?(abelianS sHG) //.
- rewrite -(eqn_pmul2r (indexg_gt0 G H)) LaGrange //; apply/eqP.
+ rewrite -(eqn_pmul2r (indexg_gt0 G H)) Lagrange //; apply/eqP.
rewrite -sum_nat_const -card_Iirr_abelian // -sum1_card.
rewrite (partition_big rH (mem (codom rH))) /=; last exact: image_f.
have nsHG: H <| G by rewrite -sub_abelian_normal.
@@ -2368,7 +2371,7 @@ have [j ->]: exists j, 'chi_i = 'Res 'chi[G]_j.
by rewrite cfker1 ?linG1 ?mul1r ?(subsetP _ x Hx) // mod_IirrE ?cfker_Mod.
have: dvdNC #|G : H| (#|G : H|%:R * '[chi, 'chi_j]).
by rewrite dvdC_mulr ?isIntC_Nat ?cfdot_char_irr_Nat.
-congr (dvdNC _ _); rewrite (cfdotEl _ Hchi) -(LaGrange sHG) mulnC natrM.
+congr (dvdNC _ _); rewrite (cfdotEl _ Hchi) -(Lagrange sHG) mulnC natrM.
rewrite invfM -mulrA mulVKf ?neq0GiC //; congr (_ * _).
by apply: eq_bigr => x Hx; rewrite !cfResE.
Qed.
diff --git a/maximal.v b/maximal.v
index ba684dd5..e039f2e9 100644
--- a/maximal.v
+++ b/maximal.v
@@ -138,12 +138,12 @@ Qed.
Lemma p_index_maximal : M \subset P -> prime #|P : M| -> maximal M P.
Proof.
move=> sMP /primeP[lt1PM pr_PM].
-apply/maxgroupP; rewrite properEcard sMP -(LaGrange sMP).
+apply/maxgroupP; rewrite properEcard sMP -(Lagrange sMP).
rewrite -{1}(muln1 #|M|) ltn_pmul2l //; split=> // H sHP sMH.
apply/eqP; rewrite eq_sym eqEcard sMH.
case/orP: (pr_PM _ (indexSg sMH (proper_sub sHP))) => /eqP iM.
- by rewrite -(LaGrange sMH) iM muln1 /=.
-by have:= proper_card sHP; rewrite -(LaGrange sMH) iM LaGrange ?ltnn.
+ by rewrite -(Lagrange sMH) iM muln1 /=.
+by have:= proper_card sHP; rewrite -(Lagrange sMH) iM Lagrange ?ltnn.
Qed.
End PMax.
@@ -994,7 +994,7 @@ Proof.
move=> sUG; rewrite setIAC (setIidPr sUG).
elim: {U}_.+1 {-2}U (ltnSn #|U|) sUG => // m IHm U leUm sUG.
have [cUG | not_cUG]:= orP (orbN (G \subset 'C(U))).
- by rewrite !(setIidPl _) ?LaGrange // centsC.
+ by rewrite !(setIidPl _) ?Lagrange // centsC.
have{not_cUG} [x Gx not_cUx] := subsetPn not_cUG.
pose W := 'C_U[x]; have sCW_G: 'C_G(W) \subset G := subsetIl G _.
have maxW: maximal W U by rewrite subcent1_extraspecial_maximal // inE not_cUx.
@@ -1008,9 +1008,9 @@ have iCW_CU: #|'C_G(W) : 'C_G(U)| = p.
apply: subcent1_extraspecial_maximal sCW_G _.
rewrite inE andbC (subsetP sUG) //= -sub_cent1.
by apply/subsetPn; exists x; rewrite // inE Gx -sub_cent1 subsetIr.
-apply/eqP; rewrite -(eqn_pmul2r p_gt0) -{1}iCW_CU LaGrange ?setIS ?centS //.
+apply/eqP; rewrite -(eqn_pmul2r p_gt0) -{1}iCW_CU Lagrange ?setIS ?centS //.
rewrite IHm ?(leq_trans (proper_card ltWU)) // -setIA -mulnA.
-rewrite -(LaGrange_index sUG sWU) (p_maximal_index (pgroupS sUG pG)) //=.
+rewrite -(Lagrange_index sUG sWU) (p_maximal_index (pgroupS sUG pG)) //=.
by rewrite -cent_set1 (setIidPr (centS _)) ?sub1set.
Qed.
@@ -1121,7 +1121,7 @@ have [sVE sWF]: V \subset E /\ W \subset F by rewrite -defE -defF !mulG_subr.
have [sVG sWG] := (subset_trans sVE sEG, subset_trans sWF sFG).
rewrite -defE -defF !TI_cardMg // leq_pmul2l ?cardG_gt0 //.
rewrite -(leq_pmul2r (cardG_gt0 'C_G(W))) mul_cardG.
-rewrite card_subcent_extraspecial // mulnCA LaGrange // mulnC.
+rewrite card_subcent_extraspecial // mulnCA Lagrange // mulnC.
rewrite leq_mul ?subset_leq_card //; last by rewrite mul_subG ?subsetIl.
apply: subset_trans (sub1G _); rewrite -tiUV !subsetI subsetIl subIset ?sVE //=.
rewrite -(pmaxElem_LdivP p_pr maxF) -defF centM -!setIA -(setICA 'C(W)).
diff --git a/orderedalg.v b/orderedalg.v
index 03c42525..46b05b51 100644
--- a/orderedalg.v
+++ b/orderedalg.v
@@ -114,18 +114,21 @@ Local Coercion base : class_of >-> GRing.IntegralDomain.class_of.
Local Coercion mixin : class_of >-> mixin_of.
Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
-Definition class cT := let: Pack _ c _ := cT return class_of cT in c.
-Definition clone T cT c of phant_id (class cT) c := @Pack T c T.
+Variables (T : Type) (cT : type).
+Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
+Definition clone c of phant_id class c := @Pack T c T.
Definition pack := gen_pack Pack Class GRing.IntegralDomain.class.
-
-Definition eqType cT := Equality.Pack (class cT) cT.
-Definition choiceType cT := Choice.Pack (class cT) cT.
-Definition zmodType cT := GRing.Zmodule.Pack (class cT) cT.
-Definition ringType cT := GRing.Ring.Pack (class cT) cT.
-Definition comRingType cT := GRing.ComRing.Pack (class cT) cT.
-Definition unitRingType cT := GRing.UnitRing.Pack (class cT) cT.
-Definition comUnitRingType cT := GRing.ComUnitRing.Pack (class cT) cT.
-Definition idomainType cT := GRing.IntegralDomain.Pack (class cT) cT.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
+Definition ringType := @GRing.Ring.Pack cT xclass xT.
+Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
+Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
+Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
End ClassDef.
@@ -2027,22 +2030,24 @@ Local Coercion base2 : class_of >-> PIntegralDomain.class_of.
Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
-Definition class cT := let: Pack _ c _ := cT return class_of cT in c.
-Definition clone T cT c of phant_id (class cT) c := @Pack T c T.
+Variables (T : Type) (cT : type).
+Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
+Definition clone c of phant_id class c := @Pack T c T.
Definition pack := gen_pack Pack Class GRing.Field.class.
-
-Definition eqType cT := Equality.Pack (class cT) cT.
-Definition choiceType cT := Choice.Pack (class cT) cT.
-Definition zmodType cT := GRing.Zmodule.Pack (class cT) cT.
-Definition ringType cT := GRing.Ring.Pack (class cT) cT.
-Definition comRingType cT := GRing.ComRing.Pack (class cT) cT.
-Definition unitRingType cT := GRing.UnitRing.Pack (class cT) cT.
-Definition comUnitRingType cT := GRing.ComUnitRing.Pack (class cT) cT.
-Definition idomainType cT := GRing.IntegralDomain.Pack (class cT) cT.
-Definition poIdomainType cT := PIntegralDomain.Pack (class cT) cT.
-Definition fieldType cT := GRing.Field.Pack (class cT) cT.
-Definition join_poIdomainType cT :=
- @PIntegralDomain.Pack (fieldType cT) (class cT) cT.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
+Definition ringType := @GRing.Ring.Pack cT xclass xT.
+Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
+Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
+Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
+Definition poIdomainType := @PIntegralDomain.Pack cT xclass xT.
+Definition fieldType := @GRing.Field.Pack cT xclass xT.
+Definition join_poIdomainType := @PIntegralDomain.Pack fieldType xclass xT.
End ClassDef.
@@ -2211,26 +2216,28 @@ Local Coercion base2 : class_of >-> PField.class_of.
Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
-Definition class cT := let: Pack _ c _ := cT return class_of cT in c.
-Definition clone T cT c of phant_id (class cT) c := @Pack T c T.
+Variables (T : Type) (cT : type).
+Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
+Definition clone c of phant_id class c := @Pack T c T.
Definition pack := gen_pack Pack Class GRing.ClosedField.class.
-
-Definition eqType cT := Equality.Pack (class cT) cT.
-Definition choiceType cT := Choice.Pack (class cT) cT.
-Definition zmodType cT := GRing.Zmodule.Pack (class cT) cT.
-Definition ringType cT := GRing.Ring.Pack (class cT) cT.
-Definition comRingType cT := GRing.ComRing.Pack (class cT) cT.
-Definition unitRingType cT := GRing.UnitRing.Pack (class cT) cT.
-Definition comUnitRingType cT := GRing.ComUnitRing.Pack (class cT) cT.
-Definition idomainType cT := GRing.IntegralDomain.Pack (class cT) cT.
-Definition poIdomainType cT := PIntegralDomain.Pack (class cT) cT.
-Definition fieldType cT := GRing.Field.Pack (class cT) cT.
-Definition decFieldType cT := GRing.DecidableField.Pack (class cT) cT.
-Definition closedFieldType cT := GRing.ClosedField.Pack (class cT) cT.
-Definition join_poIdomainType cT :=
- @PIntegralDomain.Pack (closedFieldType cT) (class cT) cT.
-Definition join_poFieldType cT :=
- @PField.Pack (closedFieldType cT) (class cT) cT.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
+Definition ringType := @GRing.Ring.Pack cT xclass xT.
+Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
+Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
+Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
+Definition poIdomainType := @PIntegralDomain.Pack cT xclass xT.
+Definition fieldType := @GRing.Field.Pack cT xclass xT.
+Definition decFieldType := @GRing.DecidableField.Pack cT xclass xT.
+Definition closedFieldType := @GRing.ClosedField.Pack cT xclass xT.
+Definition join_poIdomainType :=
+ @PIntegralDomain.Pack closedFieldType xclass xT.
+Definition join_poFieldType := @PField.Pack closedFieldType xclass xT.
End ClassDef.
@@ -2448,21 +2455,24 @@ Local Coercion base : class_of >-> PIntegralDomain.class_of.
Local Coercion mixin : class_of >-> total_mixin_of.
Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
-Definition class cT := let: Pack _ c _ := cT return class_of cT in c.
-Definition clone T cT c of phant_id (class cT) c := @Pack T c T.
+Variables (T : Type) (cT : type).
+Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
+Definition clone c of phant_id class c := @Pack T c T.
Definition pack := gen_pack' Pack Class PIntegralDomain.class.
-
-Definition eqType cT := Equality.Pack (class cT) cT.
-Definition choiceType cT := Choice.Pack (class cT) cT.
-Definition zmodType cT := GRing.Zmodule.Pack (class cT) cT.
-Definition ringType cT := GRing.Ring.Pack (class cT) cT.
-Definition comRingType cT := GRing.ComRing.Pack (class cT) cT.
-Definition unitRingType cT := GRing.UnitRing.Pack (class cT) cT.
-Definition comUnitRingType cT := GRing.ComUnitRing.Pack (class cT) cT.
-Definition idomainType cT := GRing.IntegralDomain.Pack (class cT) cT.
-Definition poidomainType cT := PIntegralDomain.Pack (class cT) cT.
-Definition join_idomainType cT :=
- @GRing.IntegralDomain.Pack (poidomainType cT) (class cT) cT.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
+Definition ringType := @GRing.Ring.Pack cT xclass xT.
+Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
+Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
+Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
+Definition poidomainType := @PIntegralDomain.Pack cT xclass xT.
+Definition join_idomainType :=
+ @GRing.IntegralDomain.Pack poidomainType xclass xT.
End ClassDef.
@@ -3099,28 +3109,28 @@ Local Coercion base2 : class_of >-> TIntegralDomain.class_of.
Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
-Definition class cT := let: Pack _ c _ := cT return class_of cT in c.
-Definition clone T cT c of phant_id (class cT) c := @Pack T c T.
+Variables (T : Type) (cT : type).
+Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
+Definition clone c of phant_id class c := @Pack T c T.
Definition pack := gen_pack' Pack Class PField.class.
-
-Definition eqType cT := Equality.Pack (class cT) cT.
-Definition choiceType cT := Choice.Pack (class cT) cT.
-Definition zmodType cT := GRing.Zmodule.Pack (class cT) cT.
-Definition ringType cT := GRing.Ring.Pack (class cT) cT.
-Definition comRingType cT := GRing.ComRing.Pack (class cT) cT.
-Definition unitRingType cT := GRing.UnitRing.Pack (class cT) cT.
-Definition comUnitRingType cT := GRing.ComUnitRing.Pack (class cT) cT.
-Definition idomainType cT := GRing.IntegralDomain.Pack (class cT) cT.
-Definition poIdomainType cT := PIntegralDomain.Pack (class cT) cT.
-Definition oIdomainType cT := TIntegralDomain.Pack (class cT) cT.
-Definition fieldType cT := GRing.Field.Pack (class cT) cT.
-Definition poFieldType cT := PField.Pack (class cT) cT.
-Definition join_poIdomainType cT :=
- @PIntegralDomain.Pack (poFieldType cT) (class cT) cT.
-Definition join_oIdomainType cT :=
- @TIntegralDomain.Pack (poFieldType cT) (class cT) cT.
-Definition join_fieldType cT :=
- @GRing.Field.Pack (poFieldType cT) (class cT) cT.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
+Definition ringType := @GRing.Ring.Pack cT xclass xT.
+Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
+Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
+Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
+Definition poIdomainType := @PIntegralDomain.Pack cT xclass xT.
+Definition oIdomainType := @TIntegralDomain.Pack cT xclass xT.
+Definition fieldType := @GRing.Field.Pack cT xclass xT.
+Definition poFieldType := @PField.Pack cT xclass xT.
+Definition join_poIdomainType := @PIntegralDomain.Pack poFieldType xclass xT.
+Definition join_oIdomainType := @TIntegralDomain.Pack poFieldType xclass xT.
+Definition join_fieldType := @GRing.Field.Pack poFieldType xclass xT.
End ClassDef.
@@ -3233,25 +3243,28 @@ Local Coercion base : class_of >-> TField.class_of.
Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
-Definition class cT := let: Pack _ c _ := cT return class_of cT in c.
-Definition clone T cT c of phant_id (class cT) c := @Pack T c T.
-Definition pack T b0 (m0 : mixin_of (@TField.Pack T b0 T)) :=
+Variables (T : Type) (cT : type).
+Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
+Definition clone c of phant_id class c := @Pack T c T.
+Definition pack b0 (m0 : mixin_of (@TField.Pack T b0 T)) :=
fun bT b & phant_id (TField.class bT) b =>
fun m & phant_id m0 m => Pack (@Class T b m) T.
-
-Definition eqType cT := Equality.Pack (class cT) cT.
-Definition choiceType cT := Choice.Pack (class cT) cT.
-Definition zmodType cT := GRing.Zmodule.Pack (class cT) cT.
-Definition ringType cT := GRing.Ring.Pack (class cT) cT.
-Definition comRingType cT := GRing.ComRing.Pack (class cT) cT.
-Definition unitRingType cT := GRing.UnitRing.Pack (class cT) cT.
-Definition comUnitRingType cT := GRing.ComUnitRing.Pack (class cT) cT.
-Definition idomainType cT := GRing.IntegralDomain.Pack (class cT) cT.
-Definition poIdomainType cT := PIntegralDomain.Pack (class cT) cT.
-Definition oIdomainType cT := TIntegralDomain.Pack (class cT) cT.
-Definition fieldType cT := GRing.Field.Pack (class cT) cT.
-Definition poFieldType cT := PField.Pack (class cT) cT.
-Definition oFieldType cT := TField.Pack (class cT) cT.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
+Definition ringType := @GRing.Ring.Pack cT xclass xT.
+Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
+Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
+Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
+Definition poIdomainType := @PIntegralDomain.Pack cT xclass xT.
+Definition oIdomainType := @TIntegralDomain.Pack cT xclass xT.
+Definition fieldType := @GRing.Field.Pack cT xclass xT.
+Definition poFieldType := @PField.Pack cT xclass xT.
+Definition oFieldType := @TField.Pack cT xclass xT.
End ClassDef.
@@ -3337,25 +3350,28 @@ Local Coercion base : class_of >-> TField.class_of.
Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
-Definition class cT := let: Pack _ c _ := cT return class_of cT in c.
-Definition clone T cT c of phant_id (class cT) c := @Pack T c T.
-Definition pack T b0 (m0 : mixin_of (@TField.Pack T b0 T)) :=
+Variables (T : Type) (cT : type).
+Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
+Definition clone c of phant_id class c := @Pack T c T.
+Definition pack b0 (m0 : mixin_of (@TField.Pack T b0 T)) :=
fun bT b & phant_id (TField.class bT) b =>
fun m & phant_id m0 m => Pack (@Class T b m) T.
-
-Definition eqType cT := Equality.Pack (class cT) cT.
-Definition choiceType cT := Choice.Pack (class cT) cT.
-Definition zmodType cT := GRing.Zmodule.Pack (class cT) cT.
-Definition ringType cT := GRing.Ring.Pack (class cT) cT.
-Definition comRingType cT := GRing.ComRing.Pack (class cT) cT.
-Definition unitRingType cT := GRing.UnitRing.Pack (class cT) cT.
-Definition comUnitRingType cT := GRing.ComUnitRing.Pack (class cT) cT.
-Definition idomainType cT := GRing.IntegralDomain.Pack (class cT) cT.
-Definition poIdomainType cT := PIntegralDomain.Pack (class cT) cT.
-Definition oIdomainType cT := TIntegralDomain.Pack (class cT) cT.
-Definition fieldType cT := GRing.Field.Pack (class cT) cT.
-Definition poFieldType cT := PField.Pack (class cT) cT.
-Definition oFieldType cT := TField.Pack (class cT) cT.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
+Definition ringType := @GRing.Ring.Pack cT xclass xT.
+Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
+Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
+Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
+Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
+Definition poIdomainType := @PIntegralDomain.Pack cT xclass xT.
+Definition oIdomainType := @TIntegralDomain.Pack cT xclass xT.
+Definition fieldType := @GRing.Field.Pack cT xclass xT.
+Definition poFieldType := @PField.Pack cT xclass xT.
+Definition oFieldType := @TField.Pack cT xclass xT.
End ClassDef.
diff --git a/pgroup.v b/pgroup.v
index ffd9c407..327692db 100644
--- a/pgroup.v
+++ b/pgroup.v
@@ -118,7 +118,7 @@ Proof.
move=> prG; have [|[p p_pr pG]] := trivgVpdiv (H :&: G); first by right.
left; rewrite (sameP setIidPr eqP) eqEcard subsetIr.
suffices <-: p = #|G| by rewrite dvdn_leq ?cardG_gt0.
-by apply/eqP; rewrite -dvdn_prime2 // -(LaGrangeI G H) setIC dvdn_mulr.
+by apply/eqP; rewrite -dvdn_prime2 // -(LagrangeI G H) setIC dvdn_mulr.
Qed.
Lemma pgroupE pi A : pi.-group A = pi.-nat #|A|. Proof. by []. Qed.
@@ -187,8 +187,8 @@ Qed.
Lemma pgroupM pi G H : pi.-group (G * H) = pi.-group G && pi.-group H.
Proof.
have GH_gt0: 0 < #|G :&: H| := cardG_gt0 _.
-rewrite /pgroup -(mulnK #|_| GH_gt0) -mul_cardG -(LaGrangeI G H) -mulnA.
-by rewrite mulKn // -(LaGrangeI H G) setIC !pnat_mul andbCA; case: (pnat _).
+rewrite /pgroup -(mulnK #|_| GH_gt0) -mul_cardG -(LagrangeI G H) -mulnA.
+by rewrite mulKn // -(LagrangeI H G) setIC !pnat_mul andbCA; case: (pnat _).
Qed.
Lemma pgroupJ pi G x : pi.-group (G :^ x) = pi.-group G.
@@ -225,8 +225,8 @@ Qed.
Lemma card_Hall pi G H : pi.-Hall(G) H -> #|H| = #|G|`_pi.
Proof.
-case/and3P=> sHG piH pi'H; rewrite -(LaGrange sHG).
-by rewrite partnM ?LaGrange // part_pnat_id ?part_p'nat ?muln1.
+case/and3P=> sHG piH pi'H; rewrite -(Lagrange sHG).
+by rewrite partnM ?Lagrange // part_pnat_id ?part_p'nat ?muln1.
Qed.
Lemma pHall_sub pi A B : pi.-Hall(A) B -> B \subset A.
@@ -618,7 +618,7 @@ have{pG n leGn IHn} pZ: p %| #|'C_G(G)|.
by apply/actsP=> x Gx y; rewrite !inE -!mem_conjgV -centJ conjGid ?groupV.
elim/big_ind: _ => //; first exact: dvdn_add.
move=> _ /imsetP[x /setDP[Gx nCx] ->]; rewrite card_orbit astab1J.
- move: pG; rewrite -(LaGrange (subsetIl G 'C[x])) Euclid_dvdM // => /orP[] //.
+ move: pG; rewrite -(Lagrange (subsetIl G 'C[x])) Euclid_dvdM // => /orP[] //.
case/IHn=> [|y /setIP[Gy _ /eqP oyp]]; last by case/andP: (no_x y).
apply: leq_trans leGn; apply: proper_card; rewrite properE subsetIl.
by rewrite subsetI subxx /= -cent_set1 centsC sub1set.
@@ -680,7 +680,7 @@ case/Cauchy=> //= Hx; rewrite -sub1set -gen_subG -/<[Hx]> /order.
case/inv_quotientS=> //= K -> sHK sKG {Hx}.
rewrite card_quotient ?(subset_trans sKG) // => iKH; apply/negP=> pi_p.
rewrite -iKH -divgS // (maxH K) ?divnn ?cardG_gt0 // in p_pr.
-by rewrite /psubgroup sKG /pgroup -(LaGrange sHK) mulnC pnat_mul iKH pi_p.
+by rewrite /psubgroup sKG /pgroup -(Lagrange sHK) mulnC pnat_mul iKH pi_p.
Qed.
Lemma setI_normal_Hall G H K :
@@ -733,7 +733,7 @@ Lemma pmorphim_pHall pi G H :
pi.-Hall(f @* G) (f @* H) = pi.-Hall(G) H.
Proof.
move=> sGD sHD /andP[/subsetIP[sKH sKG] piK]; rewrite !pHallE morphimSGK //.
-apply: andb_id2l => sHG; rewrite -(LaGrange sKH) -(LaGrange sKG) partnM //.
+apply: andb_id2l => sHG; rewrite -(Lagrange sKH) -(Lagrange sKG) partnM //.
by rewrite (part_pnat_id piK) !card_morphim !(setIidPr _) // eqn_pmul2l.
Qed.
diff --git a/polydiv.v b/polydiv.v
index a7b589bb..1531035d 100644
--- a/polydiv.v
+++ b/polydiv.v
@@ -1503,7 +1503,6 @@ by rewrite !exprS (@eqp_trans (q * p ^+ k)) // (eqp_mulr, eqp_mull).
Qed.
Lemma polyC_eqp1 c : (c%:P %= 1) = (c != 0).
-
Proof.
apply/eqpP/idP => [[[x y]] |nc0] /=.
case c0: (c == 0); rewrite // scale_poly1 (eqP c0) scaler0.
diff --git a/primitive_action.v b/primitive_action.v
index 0ed1059f..c4f8f451 100644
--- a/primitive_action.v
+++ b/primitive_action.v
@@ -67,8 +67,8 @@ apply/forallP/maximal_eqP=> /= [primG | [_ maxCx] Q].
have [|/proper_card oCH] := eqVproper sCH; [by left | right].
apply/eqP; rewrite eqEcard sHG leqNgt.
apply: contra {primG}(primG Q) => oHG; apply/and3P; split; last first.
- - rewrite card_orbit astab1_set defH -(@ltn_pmul2l #|H|) ?LaGrange // muln1.
- rewrite oHG -(@ltn_pmul2l #|H|) ?LaGrange // -(card_orbit_stab to G x).
+ - rewrite card_orbit astab1_set defH -(@ltn_pmul2l #|H|) ?Lagrange // muln1.
+ rewrite oHG -(@ltn_pmul2l #|H|) ?Lagrange // -(card_orbit_stab to G x).
by rewrite -(atransP trG x Sx) mulnC card_orbit ltn_pmul2r.
- by apply/actsP=> a Ga Y; apply: orbit_transr; exact: mem_orbit.
apply/and3P; split; last 1 first.
diff --git a/quotient.v b/quotient.v
index 8bb9596d..0bd42c59 100644
--- a/quotient.v
+++ b/quotient.v
@@ -890,10 +890,10 @@ Lemma index_morphim_ker G H :
(#|f @* G : f @* H| * #|'ker_G f : H|)%N = #|G : H|.
Proof.
move=> sHG sGD; apply/eqP.
-rewrite -(eqn_pmul2l (cardG_gt0 (f @* H))) mulnA LaGrange ?morphimS //.
+rewrite -(eqn_pmul2l (cardG_gt0 (f @* H))) mulnA Lagrange ?morphimS //.
rewrite !card_morphim (setIidPr sGD) (setIidPr (subset_trans sHG sGD)).
rewrite -(eqn_pmul2l (cardG_gt0 ('ker_H f))) /=.
-by rewrite -{1}(setIidPr sHG) setIAC mulnCA mulnC mulnA !LaGrangeI LaGrange.
+by rewrite -{1}(setIidPr sHG) setIAC mulnCA mulnC mulnA !LagrangeI Lagrange.
Qed.
Lemma index_morphim G H : G :&: H \subset D -> #|f @* G : f @* H| %| #|G : H|.
@@ -915,7 +915,7 @@ Qed.
Lemma card_morphpre L : L \subset f @* D -> #|f @*^-1 L| = (#|'ker f| * #|L|)%N.
Proof.
move/morphpreK=> {2} <-; rewrite card_morphim morphpreIdom.
-by rewrite LaGrange // morphpreS ?sub1G.
+by rewrite Lagrange // morphpreS ?sub1G.
Qed.
Lemma index_morphpre L M :
diff --git a/ssralg.v b/ssralg.v
index 474ca9ca..5d55da9c 100644
--- a/ssralg.v
+++ b/ssralg.v
@@ -609,12 +609,14 @@ Local Coercion sort : type >-> Sortclass.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c T.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
Definition pack m :=
fun bT b & phant_id (Choice.class bT) b => Pack (@Class T b m) T.
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
End ClassDef.
@@ -861,14 +863,17 @@ Local Coercion sort : type >-> Sortclass.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c T.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+
Definition pack b0 (m0 : mixin_of (@Zmodule.Pack T b0 T)) :=
fun bT b & phant_id (Zmodule.class bT) b =>
fun m & phant_id m0 m => Pack (@Class T b m) T.
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition zmodType := Zmodule.Pack class cT.
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @Zmodule.Pack cT xclass xT.
End ClassDef.
@@ -1442,14 +1447,17 @@ Local Coercion sort : type >-> Sortclass.
Variable (phR : phant R) (T : Type) (cT : type phR).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack phR T c T.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+
Definition pack b0 (m0 : mixin_of R (@Zmodule.Pack T b0 T)) :=
fun bT b & phant_id (Zmodule.class bT) b =>
fun m & phant_id m0 m => Pack phR (@Class T b m) T.
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition zmodType := Zmodule.Pack class cT.
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @Zmodule.Pack cT xclass xT.
End ClassDef.
@@ -1598,6 +1606,8 @@ Local Coercion sort : type >-> Sortclass.
Variable (phR : phant R) (T : Type) (cT : type phR).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack phR T c T.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
Definition pack T b0 mul0 (axT : @axiom R (@Lmodule.Pack R _ T b0 T) mul0) :=
fun bT b & phant_id (Ring.class bT) (b : Ring.class_of T) =>
@@ -1605,12 +1615,12 @@ Definition pack T b0 mul0 (axT : @axiom R (@Lmodule.Pack R _ T b0 T) mul0) :=
fun ax & phant_id axT ax =>
Pack (Phant R) (@Class T b m ax) T.
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition zmodType := Zmodule.Pack class cT.
-Definition ringType := Ring.Pack class cT.
-Definition lmodType := Lmodule.Pack phR class cT.
-Definition lmod_ringType := @Lmodule.Pack R phR ringType class cT.
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @Ring.Pack cT xclass xT.
+Definition lmodType := @Lmodule.Pack R phR cT xclass xT.
+Definition lmod_ringType := @Lmodule.Pack R phR ringType xclass xT.
End ClassDef.
@@ -2374,15 +2384,17 @@ Local Coercion sort : type >-> Sortclass.
Variable (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c T.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
Definition pack mul0 (m0 : @commutative T T mul0) :=
fun bT b & phant_id (Ring.class bT) b =>
fun m & phant_id m0 m => Pack (@Class T b m) T.
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition zmodType := Zmodule.Pack class cT.
-Definition ringType := Ring.Pack class cT.
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @Ring.Pack cT xclass xT.
End ClassDef.
@@ -2528,17 +2540,19 @@ Local Coercion sort : type >-> Sortclass.
Variable (phR : phant R) (T : Type) (cT : type phR).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack phR T c T.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
Definition pack b0 (ax0 : @axiom R b0) :=
fun bT b & phant_id (@Lalgebra.class R phR bT) b =>
fun ax & phant_id ax0 ax => Pack phR (@Class T b ax) T.
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition zmodType := Zmodule.Pack class cT.
-Definition ringType := Ring.Pack class cT.
-Definition lmodType := Lmodule.Pack phR class cT.
-Definition lalgType := Lalgebra.Pack phR class cT.
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @Ring.Pack cT xclass xT.
+Definition lmodType := @Lmodule.Pack R phR cT xclass xT.
+Definition lalgType := @Lalgebra.Pack R phR cT xclass xT.
End ClassDef.
@@ -2646,15 +2660,17 @@ Local Coercion sort : type >-> Sortclass.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c T.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
Definition pack b0 (m0 : mixin_of (@Ring.Pack T b0 T)) :=
fun bT b & phant_id (Ring.class bT) b =>
fun m & phant_id m0 m => Pack (@Class T b m) T.
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition zmodType := Zmodule.Pack class cT.
-Definition ringType := Ring.Pack class cT.
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @Ring.Pack cT xclass xT.
End ClassDef.
@@ -2953,19 +2969,21 @@ Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
Definition pack :=
fun bT b & phant_id (ComRing.class bT) (b : ComRing.class_of T) =>
fun mT m & phant_id (UnitRing.class mT) (@UnitRing.Class T b m) =>
Pack (@Class T b m) T.
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition zmodType := Zmodule.Pack class cT.
-Definition ringType := Ring.Pack class cT.
-Definition comRingType := ComRing.Pack class cT.
-Definition unitRingType := UnitRing.Pack class cT.
-Definition com_unitRingType := @UnitRing.Pack comRingType class cT.
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @Ring.Pack cT xclass xT.
+Definition comRingType := @ComRing.Pack cT xclass xT.
+Definition unitRingType := @UnitRing.Pack cT xclass xT.
+Definition com_unitRingType := @UnitRing.Pack comRingType xclass xT.
End ClassDef.
@@ -3015,23 +3033,25 @@ Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variable (phR : phant R) (T : Type) (cT : type phR).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
Definition pack :=
fun bT b & phant_id (@Algebra.class R phR bT) (b : Algebra.class_of R T) =>
fun mT m & phant_id (UnitRing.class mT) (@UnitRing.Class T b m) =>
Pack (Phant R) (@Class T b m) T.
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition zmodType := Zmodule.Pack class cT.
-Definition ringType := Ring.Pack class cT.
-Definition unitRingType := UnitRing.Pack class cT.
-Definition lmodType := Lmodule.Pack phR class cT.
-Definition lalgType := Lalgebra.Pack phR class cT.
-Definition algType := Algebra.Pack phR class cT.
-Definition lmod_unitRingType := @Lmodule.Pack R phR unitRingType class cT.
-Definition lalg_unitRingType := @Lalgebra.Pack R phR unitRingType class cT.
-Definition alg_unitRingType := @Algebra.Pack R phR unitRingType class cT.
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @Ring.Pack cT xclass xT.
+Definition unitRingType := @UnitRing.Pack cT xclass xT.
+Definition lmodType := @Lmodule.Pack R phR cT xclass xT.
+Definition lalgType := @Lalgebra.Pack R phR cT xclass xT.
+Definition algType := @Algebra.Pack R phR cT xclass xT.
+Definition lmod_unitRingType := @Lmodule.Pack R phR unitRingType xclass xT.
+Definition lalg_unitRingType := @Lalgebra.Pack R phR unitRingType xclass xT.
+Definition alg_unitRingType := @Algebra.Pack R phR unitRingType xclass xT.
End ClassDef.
@@ -4212,18 +4232,20 @@ Local Coercion sort : type >-> Sortclass.
Variable (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c T.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
Definition pack b0 (m0 : axiom (@Ring.Pack T b0 T)) :=
fun bT b & phant_id (ComUnitRing.class bT) b =>
fun m & phant_id m0 m => Pack (@Class T b m) T.
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition zmodType := Zmodule.Pack class cT.
-Definition ringType := Ring.Pack class cT.
-Definition comRingType := ComRing.Pack class cT.
-Definition unitRingType := UnitRing.Pack class cT.
-Definition comUnitRingType := ComUnitRing.Pack class cT.
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @Ring.Pack cT xclass xT.
+Definition comRingType := @ComRing.Pack cT xclass xT.
+Definition unitRingType := @UnitRing.Pack cT xclass xT.
+Definition comUnitRingType := @ComUnitRing.Pack cT xclass xT.
End ClassDef.
@@ -4390,19 +4412,21 @@ Local Coercion sort : type >-> Sortclass.
Variable (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c T.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
Definition pack b0 (m0 : mixin_of (@UnitRing.Pack T b0 T)) :=
fun bT b & phant_id (IntegralDomain.class bT) b =>
fun m & phant_id m0 m => Pack (@Class T b m) T.
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition zmodType := Zmodule.Pack class cT.
-Definition ringType := Ring.Pack class cT.
-Definition comRingType := ComRing.Pack class cT.
-Definition unitRingType := UnitRing.Pack class cT.
-Definition comUnitRingType := ComUnitRing.Pack class cT.
-Definition idomainType := IntegralDomain.Pack class cT.
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @Ring.Pack cT xclass xT.
+Definition comRingType := @ComRing.Pack cT xclass xT.
+Definition unitRingType := @UnitRing.Pack cT xclass xT.
+Definition comUnitRingType := @ComUnitRing.Pack cT xclass xT.
+Definition idomainType := @IntegralDomain.Pack cT xclass xT.
End ClassDef.
@@ -4636,20 +4660,22 @@ Local Coercion sort : type >-> Sortclass.
Variable (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c T.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
Definition pack b0 (m0 : mixin_of (@UnitRing.Pack T b0 T)) :=
fun bT b & phant_id (Field.class bT) b =>
fun m & phant_id m0 m => Pack (@Class T b m) T.
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition zmodType := Zmodule.Pack class cT.
-Definition ringType := Ring.Pack class cT.
-Definition comRingType := ComRing.Pack class cT.
-Definition unitRingType := UnitRing.Pack class cT.
-Definition comUnitRingType := ComUnitRing.Pack class cT.
-Definition idomainType := IntegralDomain.Pack class cT.
-Definition fieldType := Field.Pack class cT.
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @Ring.Pack cT xclass xT.
+Definition comRingType := @ComRing.Pack cT xclass xT.
+Definition unitRingType := @UnitRing.Pack cT xclass xT.
+Definition comUnitRingType := @ComUnitRing.Pack cT xclass xT.
+Definition idomainType := @IntegralDomain.Pack cT xclass xT.
+Definition fieldType := @Field.Pack cT xclass xT.
End ClassDef.
@@ -4876,6 +4902,8 @@ Local Coercion sort : type >-> Sortclass.
Variable (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c T.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
Definition pack b0 (m0 : axiom (@Ring.Pack T b0 T)) :=
fun bT b & phant_id (DecidableField.class bT) b =>
@@ -4884,16 +4912,16 @@ Definition pack b0 (m0 : axiom (@Ring.Pack T b0 T)) :=
(* There should eventually be a constructor from polynomial resolution *)
(* that builds the DecidableField mixin using QE. *)
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition zmodType := Zmodule.Pack class cT.
-Definition ringType := Ring.Pack class cT.
-Definition comRingType := ComRing.Pack class cT.
-Definition unitRingType := UnitRing.Pack class cT.
-Definition comUnitRingType := ComUnitRing.Pack class cT.
-Definition idomainType := IntegralDomain.Pack class cT.
-Definition fieldType := Field.Pack class cT.
-Definition decFieldType := DecidableField.Pack class cT.
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @Zmodule.Pack cT xclass xT.
+Definition ringType := @Ring.Pack cT xclass xT.
+Definition comRingType := @ComRing.Pack cT xclass xT.
+Definition unitRingType := @UnitRing.Pack cT xclass xT.
+Definition comUnitRingType := @ComUnitRing.Pack cT xclass xT.
+Definition idomainType := @IntegralDomain.Pack cT xclass xT.
+Definition fieldType := @Field.Pack cT xclass xT.
+Definition decFieldType := @DecidableField.Pack cT class xT.
End ClassDef.
diff --git a/sylow.v b/sylow.v
index c085d228..43104ae5 100644
--- a/sylow.v
+++ b/sylow.v
@@ -141,7 +141,7 @@ have sylP: p.-Sylow(G) P.
case p_pr: (prime p); last first.
rewrite p_part lognE p_pr /= -trivg_card1; apply/idPn=> ntP.
by case/pgroup_pdiv: pP p_pr => // ->.
- rewrite -(LaGrangeI G 'N(P)) /= mulnC partnM ?cardG_gt0 // part_p'nat.
+ rewrite -(LagrangeI G 'N(P)) /= mulnC partnM ?cardG_gt0 // part_p'nat.
by rewrite mul1n (card_Hall (sylS P S_P)).
by rewrite p'natE // -indexgI -oSiN // /dvdn oS1.
have eqS Q: maxp G Q = p.-Sylow(G) Q.
@@ -238,7 +238,7 @@ apply: (iffP idP) => [syl1 | [P sylP nPG]]; last first.
by rewrite (card_Syl sylP) (setIidPl _) (indexgg, normal_norm).
have [P sylP] := Sylow_exists p G; exists P => //.
rewrite /normal (pHall_sub sylP); apply/setIidPl; apply/eqP.
-rewrite eqEcard subsetIl -(LaGrangeI G 'N(P)) -indexgI /=.
+rewrite eqEcard subsetIl -(LagrangeI G 'N(P)) -indexgI /=.
by rewrite -(card_Syl sylP) (eqP syl1) muln1.
Qed.
@@ -260,7 +260,7 @@ case: (eqVneq (P / Z) 1) => [-> |]; first exact: cyclic1.
have pPq := quotient_pgroup 'Z(P) pP; case/(pgroup_pdiv pPq) => _ _ [j oPq].
rewrite prime_cyclic // oPq; case: j oPq lePp2 => //= j.
rewrite card_quotient ?gfunctor.gFnorm //.
-by rewrite -(LaGrange sZP) lognM // => ->; rewrite oZ !pfactorK ?addnS.
+by rewrite -(Lagrange sZP) lognM // => ->; rewrite oZ !pfactorK ?addnS.
Qed.
Lemma card_p2group_abelian P : prime p -> #|P| = (p ^ 2)%N -> abelian P.
@@ -565,12 +565,12 @@ have{cPz} nzP: P \subset 'N(<[z]>) by rewrite cents_norm // centsC.
have: N / <[z]> <| P / <[z]> by rewrite morphim_normal.
case/IHr=> [||Qb [sQNb nQPb]]; first exact: morphim_pgroup.
rewrite card_quotient ?(subset_trans (normal_sub nNP)) // -ltnS.
- apply: (leq_trans le_r); rewrite -(LaGrange szN) [#|_|]ozp.
+ apply: (leq_trans le_r); rewrite -(Lagrange szN) [#|_|]ozp.
by rewrite lognM // ?prime_gt0 // logn_prime ?eqxx.
case/(inv_quotientN _): nQPb sQNb => [|Q -> szQ nQP]; first exact/andP.
have nzQ := subset_trans (normal_sub nQP) nzP.
rewrite quotientSGK // card_quotient // => sQN izQ.
-by exists Q; split=> //; rewrite expnS -izQ -ozp LaGrange.
+by exists Q; split=> //; rewrite expnS -izQ -ozp Lagrange.
Qed.
Theorem Baer_Suzuki x G :
diff --git a/vcharacter.v b/vcharacter.v
index c889ba48..618e5066 100644
--- a/vcharacter.v
+++ b/vcharacter.v
@@ -573,7 +573,7 @@ have oK1: #|K1| = #|G : H|.
rewrite -(eqnP tiHG) (eq_bigr (fun _ => #|H|.-1)); last first.
by move=> _ /imsetP[x _ ->]; rewrite cardJg (cardsD1 1%g H) group1.
rewrite sum_nat_const card_orbit astab1Js normD1 defNH.
- by rewrite -subn1 mulnBr mulnC LaGrange // muln1 subKn ?leq_imset_card.
+ by rewrite -subn1 mulnBr mulnC Lagrange // muln1 subKn ?leq_imset_card.
suffices extG i: {j | {in H, 'chi[G]_j =1 'chi[H]_i} & K1 \subset cfker 'chi_j}.
pose K := [group of \bigcap_i cfker 'chi_(s2val (extG i))].
have nKH: H \subset 'N(K).
@@ -584,7 +584,7 @@ suffices extG i: {j | {in H, 'chi[G]_j =1 'chi[H]_i} & K1 \subset cfker 'chi_j}.
by case: (extG i) => /= j def_j _; rewrite !def_j.
exists K; rewrite sdprodE // eqEcard TI_cardMg // mul_subG //=; last first.
by rewrite (bigcap_min (0 : Iirr H)) ?cfker_sub.
- rewrite -(LaGrange sHG) mulnC leq_pmul2r // -oK1 subset_leq_card //.
+ rewrite -(Lagrange sHG) mulnC leq_pmul2r // -oK1 subset_leq_card //.
by apply/bigcapsP=> i _; case: (extG i).
case i0: (i == 0).
exists 0 => [x Hx|]; last by rewrite chi0_1 cfker_cfun1 subsetDl.
diff --git a/vector.v b/vector.v
index 7070811d..257d866b 100644
--- a/vector.v
+++ b/vector.v
@@ -120,16 +120,18 @@ Local Coercion sort : type >-> Sortclass.
Variables (phR : phant R) (T : Type) (cT : type phR).
Definition class := let: Pack _ c _ := cT return class_of cT in c.
Definition clone c of phant_id class c := @Pack phR T c T.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
Definition dim := let: Mixin n _ := mixin class in n.
Definition pack b0 (m0 : mixin_of (@GRing.Lmodule.Pack R _ T b0 T)) :=
fun bT b & phant_id (@GRing.Lmodule.class _ phR bT) b =>
fun m & phant_id m0 m => Pack phR (@Class T b m) T.
-Definition eqType := Equality.Pack class cT.
-Definition choiceType := Choice.Pack class cT.
-Definition zmodType := GRing.Zmodule.Pack class cT.
-Definition lmodType := GRing.Lmodule.Pack phR class cT.
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
+Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT.
End ClassDef.
Notation axiom n V := (axiom_def n (Phant V)).
diff --git a/wielandt_fixpoint.v b/wielandt_fixpoint.v
index 206e36da..66de6415 100644
--- a/wielandt_fixpoint.v
+++ b/wielandt_fixpoint.v
@@ -512,7 +512,7 @@ wlog minV: / minnormal V (V <*> G).
rewrite -(coprime_quotient_cent sBV nBAj copVAj solV).
have -> : 'C_B(A j) = 'C_V(A j) :&: B.
by rewrite [_ :&: B]setIC setIA (setIidPl sBV).
- by rewrite card_quotient ?LaGrangeI // subIset ?nBV.
+ by rewrite card_quotient ?LagrangeI // subIset ?nBV.
have hp : forall mm j, 0 < m j + n j ->
(#|'C_V(A j)| ^ (mm j * #|A j|))%N =
((#|'C_B(A j)| ^ (mm j * #|A j|) *
--
2.26.1
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment