Description: The matrix ring is a group. (Contributed by AV, 21-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Hypothesis | matlmod.a | ⊢ 𝐴 = ( 𝑁 Mat 𝑅 ) | |
Assertion | matgrp | ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Grp ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | matlmod.a | ⊢ 𝐴 = ( 𝑁 Mat 𝑅 ) | |
2 | 1 | matlmod | ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ LMod ) |
3 | lmodgrp | ⊢ ( 𝐴 ∈ LMod → 𝐴 ∈ Grp ) | |
4 | 2 3 | syl | ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Grp ) |