Add elementary abelian finite modules lemmas to abelian

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

1 files changed, 20 insertions, 2 deletions

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.