Add elementary abelian finite modules lemmas to abelian

This factors proofs in mxabelem and finfield and removes
dependencies between these two files.

3 files changed, 30 insertions, 17 deletions

diff --git a/mathcomp/character/finfield.v b/mathcomp/character/finfield.v
index 1bebb01..9fb1b99 100644
--- a/mathcomp/character/finfield.v
+++ b/mathcomp/character/finfield.v
@@ -8,7 +8,7 @@ Require Import tuple bigop prime finset fingroup ssralg poly polydiv.
 From mathcomp
 Require Import morphism action finalg zmodp cyclic center pgroup abelian.
 From mathcomp
-Require Import matrix mxabelem vector falgebra fieldext separable galois.
+Require Import matrix vector falgebra fieldext separable galois.
 From mathcomp
 Require ssrnum ssrint algC cyclotomic.
 
@@ -121,8 +121,7 @@ Qed.
 Lemma finField_is_abelem : is_abelem [set: F].
 Proof.
 have [p pr_p charFp] := finCharP.
-apply/is_abelemP; exists p; rewrite ?abelemE ?zmod_abelian //=.
-by apply/exponentP=> x _; rewrite zmodXgE mulrn_char.
+by apply/is_abelemP; exists p; last exact: fin_ring_char_abelem.
 Qed.
 
 Lemma card_finCharP p n : #|F| = (p ^ n)%N -> prime p -> p \in [char F].
@@ -231,7 +230,7 @@ Local Infix "*p:" := primeChar_scale (at level 40).
 
 Let natrFp n : (inZp n : 'F_p)%:R = n%:R :> R.
 Proof.
-rewrite {2}(divn_eq n p) natrD mulrnA (mulrn_char charRp) add0r.
+rewrite [in RHS](divn_eq n p) natrD mulrnA (mulrn_char charRp) add0r.
 by rewrite /= (Fp_cast (charf_prime charRp)).
 Qed.
 
@@ -287,14 +286,14 @@ Canonical primeChar_finZmodType := [finZmodType of R].
 Canonical primeChar_baseGroupType := [baseFinGroupType of R for +%R].
 Canonical primeChar_groupType := [finGroupType of R for +%R].
 Canonical primeChar_finRingType := [finRingType of R].
+Canonical primeChar_finLmodType := [finLmodType 'F_p of R].
+Canonical primeChar_finLalgType := [finLalgType 'F_p of R].
+Canonical primeChar_finAlgType := [finAlgType 'F_p of R].
 
 Let pr_p : prime p. Proof. exact: charf_prime charRp. Qed.
 
 Lemma primeChar_abelem : p.-abelem [set: R].
-Proof.
-rewrite abelemE ?zmod_abelian //=.
-by apply/exponentP=> x _; rewrite zmodXgE mulrn_char.
-Qed.
+Proof. exact: fin_Fp_lmod_abelem. Qed.
 
 Lemma primeChar_pgroup : p.-group [set: R].
 Proof. by case/and3P: primeChar_abelem. Qed.
@@ -310,8 +309,8 @@ Proof. by rewrite /n -cardsT {1}(card_pgroup primeChar_pgroup). Qed.
 Lemma primeChar_vectAxiom : Vector.axiom n (primeChar_lmodType charRp).
 Proof.
 have /isog_isom/=[f /isomP[injf im_f]]: [set: R] \isog [set: 'rV['F_p]_n].
-  have [abelR ntR] := (primeChar_abelem, finRing_nontrivial R0).
-  by rewrite /n -cardsT -(dim_abelemE abelR) ?isog_abelem_rV.
+  rewrite (@isog_abelem_card _ _ p) fin_Fp_lmod_abelem //=.
+  by rewrite !cardsT card_primeChar card_matrix mul1n card_Fp.
 exists f; last by exists (invm injf) => x; rewrite ?invmE ?invmK ?im_f ?inE.
 move=> a x y; rewrite [a *: _]mulr_natl morphM ?morphX ?inE // zmodXgE.
 by congr (_ + _); rewrite -scaler_nat natr_Zp.
diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v
index aae2899..aa14808 100644
--- a/mathcomp/character/mxabelem.v
+++ b/mathcomp/character/mxabelem.v
@@ -427,11 +427,7 @@ Variables p m n : nat.
 Local Notation Mmn := 'M['F_p]_(m, n).
 
 Lemma mx_Fp_abelem : prime p -> p.-abelem [set: Mmn].
-Proof.
-move=> p_pr; apply/abelemP=> //; rewrite zmod_abelian.
-split=> //= v _; rewrite zmodXgE -scaler_nat.
-by case/andP: (char_Fp p_pr) => _ /eqP->; rewrite scale0r.
-Qed.
+Proof. exact: fin_Fp_lmod_abelem. Qed.
 
 Lemma mx_Fp_stable (L : {group Mmn}) : [acts setT, on L | 'Zm].
 Proof.
diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v
index 52f12aa..e608c4f 100644
--- a/mathcomp/solvable/abelian.v
+++ b/mathcomp/solvable/abelian.v
@@ -6,9 +6,9 @@ Require Import ssrbool ssrfun eqtype ssrnat seq path div fintype.
 From mathcomp
 Require Import finfun bigop finset prime binomial fingroup morphism perm.
 From mathcomp
-Require Import automorphism action quotient gfunctor gproduct zmodp cyclic.
+Require Import automorphism action quotient gfunctor gproduct ssralg finalg.
 From mathcomp
-Require Import pgroup gseries nilpotent sylow.
+Require Import zmodp cyclic pgroup gseries nilpotent sylow.
 
 (******************************************************************************)
 (* Constructions based on abelian groups and their structure, with some       *)
@@ -2162,6 +2162,24 @@ Proof. exact: morphim_p_rank_abelian. Qed.
 
 End QuotientRank.
 
+Section FimModAbelem.
 
+Import GRing.Theory FinRing.Theory.
 
+Lemma fin_lmod_char_abelem p (R : ringType) (V : finLmodType R):
+  p \in [char R]%R -> p.-abelem [set: V].
+Proof.
+case/andP=> p_pr /eqP-pR0; apply/abelemP=> //.
+by split=> [|v _]; rewrite ?zmod_abelian // zmodXgE -scaler_nat pR0 scale0r.
+Qed.
+
+Lemma fin_Fp_lmod_abelem p (V : finLmodType 'F_p) :
+  prime p -> p.-abelem [set: V].
+Proof. by move/char_Fp/fin_lmod_char_abelem->. Qed.
+
+Lemma fin_ring_char_abelem p (R : finRingType) :
+  p \in [char R]%R -> p.-abelem [set: R].
+Proof. exact: fin_lmod_char_abelem [finLmodType R of R^o]. Qed.
+
+End FimModAbelem.