From 058ec3b9957553cdc8a82dae6d50f48d559f4fe4 Mon Sep 17 00:00:00 2001
From: Georges Gonthier
Date: Tue, 1 Dec 2015 13:47:13 +0000
Subject: Add elementary abelian finite modules lemmas to abelian

This factors proofs in mxabelem and finfield and removes
dependencies between these two files.
---
 mathcomp/character/mxabelem.v | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'mathcomp/character/mxabelem.v')

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.
-- 
cgit v1.2.3