up:: [[groupe linéaire des matrices modulaires]]
#s/maths/algèbre 

Soit $p$ un [[nombre premier]]
Soit $(GL_{n}(p), \times)$ l'ensemble des matrices modulaires de taille $n$ sur $\mathbb{Z} / p\mathbb{Z}$ muni de la [[multiplication de matrices]]
alors on veut montrer que $(GL_{n}(p), \times)$ est un groupe fini

# $\times$ est une [[loi de composition interne|lci]]

Soient $M, N \in GL_{n}(p)$

On pose $A, B \in \mathcal{M}_{n}(\mathbb{Z})$ tels que $M = \overline{A}$ et $N = \overline{B}$
(les coefficients de $M$ sont obtenus via les coefficients de $A$, par réduction modulo $p$, idem pour $N$ et $B$)
On a $MN = \overline{AB}$
On a $\det M = \overline{\det A}$ et $\det N = \overline{\det B}$
Ainsi : $\det(MN) = \det(\overline{AB}) = \overline{\det(AB)} = \overline{\det(A) \det(B)}$
Or $p \nmid \det A$ car $\overline{\det A} = \det \overline{A} = \det M \not \equiv \overline{0} \mod{p}$ car $M \in GL_{n}(p)$
de même, $p \nmid \det B$
Donc, $p \nmid \det (A) \det(B)$ car $p$ est premier
Donc, $\overline{\det(A) \det(B)} \not\equiv \overline{0} \mod{p}$

# La matrice $\overline{I_{n}} = \begin{pmatrix} \overline{1} &&\\ &\ddots& \\ && \overline{ 1}\end{pmatrix}$ est dans $GL_{n}(p)$ et est son élément neutre

En effet, $\det \overline{I_{n}} = \overline{1}^{n} = \overline{1} \neq \overline{0}$
donc $\overline{I_{n}} \in GL_{n}(p)$

$\forall M \in GL_{n}(p)$ 
on pose $A \in \mathcal{M}_{n}(\mathbb{Z})$ tel que $M = \overline{A}$
on a :
$M \overline{I_{n}} = \overline{A} \cdot\overline{I_{n}} = \overline{AI_{n}} = \overline{A} = M$
et $M \overline{I_{n}} = \overline{A} = \overline{I_{n} A} = \overline{I_{n}}\cdot \overline{A} = \overline{I_{n}} M$
Donc, $\overline{I_{n}}$ est bien l'élément neutre de $GL_{n}(p)$

# Existence de l'inverse
Soit $M \in GL_{n}(p)$  
Soit $A \in \mathcal{M}_{n}(\mathbb{Z})$ tel que $M = \overline{A}$
On a $A \in \mathcal{M}_{n}(\mathbb{R})$, donc d'après la formule de la [[comatrice]] :
$\exists B \in \mathcal{M}_{n}(\mathbb{Z}), \quad AB = (\det A) I _{n}$
On a $\overline{ 0} \neq \det M = \det \overline{A} = \overline{\det A}$ 
Ainsi, $\overline{\det A} \in \mathbb{Z} / p\mathbb{Z} \setminus \{ 0 \} = \left( \mathbb{Z} / p\mathbb{Z} \right)^{*}$ car $p$ est premier
Puisque $(\mathbb{Z} / p\mathbb{Z})^{*}$ est un groupe pour la multiplication, on sait qu'il existe $\alpha \in (\mathbb{Z} / p\mathbb{Z})^{*}$ tel que $\alpha \overline{\det A} = \overline{1}$

On a alors, avec $N := \alpha \overline{B} \in \mathcal{ M}_{n}$