General Linear Group over Arbitrary Rings

Alexander M. Nelson

doi:10.2478/forma-2026-0003

.blurhash-client-img { display: none !important; }

General Linear Group over Arbitrary Rings

Formalized Mathematics

Volume 34 (2026): Issue 1 (June 2026)

By: Alexander M. Nelson

Open Access

|Oct 2026

Abstract

We formalize the general linear group over an arbitrary (unital, associative) ring R as the group of units for the matrix ring over R. We loosely follow Elements of Mathematics by Bourbaki.

References

Jose Maria Almira and J. Ángel Cid. A ring-theoretic approach to the double-sidedness of the matrix inverse. Elemente der Mathematik, 79(1):30–33, 2023. doi:10.4171/EM/496.
Search in Google Scholar Back to article
Broderick Arneson and Piotr Rudnicki. Primitive roots of unity and cyclotomic polynomials. Formalized Mathematics, 12(1):59–67, 2004.
Search in Google Scholar Back to article
Broderick Arneson, Matthias Baaz, and Piotr Rudnicki. Witt’s proof of the Wedderburn theorem. Formalized Mathematics, 12(1):69–75, 2004.
Search in Google Scholar Back to article
Grzegorz Bancerek, Czesław Bylinski, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9–32, 2018. doi:10.1007/s10817-017-9440-6.
Search in Google Scholar Back to article
Hyman Bass. K-theory and stable algebra. Publications Mathématiques de l’IHÉS, 22: 5–60, 1964. doi:10.1007/BF02684689.
Search in Google Scholar Back to article
Nicolas Bourbaki. Elements of Mathematics. Algebra I. Chapters 1-3. Springer-Verlag, Berlin, Heidelberg, New York, London, Paris, Tokyo, 1989.
Search in Google Scholar Back to article
Nicolas Bourbaki. Algebra: Chapter 8. Springer Nature, 2023.
Search in Google Scholar Back to article
Viviana del Barco, Gustavo Infanti, Exequiel Rivas, and Paul Schwahn. Formalizing a classification theorem for low-dimensional solvable Lie algebras in Lean. In Intelligent Computer Mathematics, volume 16136 of Lecture Notes in Computer Science, pages 317–339. Springer, 2026. doi:10.1007/978-3-032-07021-0 18.
Search in Google Scholar Back to article
Truong Huu Dung, Bui Xuan Hai, and Tran Nam Son. Reversibility in matrix rings and group algebras. Periodica Mathematica Hungarica, 90:203–216, 2025. doi:10.1007/s10998-024-00614-0.
Search in Google Scholar Back to article
Francis E.A. Johnson. On the general linear group over polynomial rings. Mathematics, 14(6):942, 2026. doi:10.3390/math14060942.
Search in Google Scholar Back to article
Niklas Krofta. Topological groups. Archive of Formal Proofs, August 2024. Formal proof development in Isabelle/HOL.
Search in Google Scholar Back to article
Tsit-Yuen Lam. A First Course in Noncommutative Rings, volume 131 of Graduate Texts in Mathematics. Springer, New York, 2 edition, 2001.
Search in Google Scholar Back to article
Oliver Nash. Engel’s theorem in Mathlib. Journal of Automated Reasoning, 67(2):18, 2023. doi:10.1007/s10817-023-09668-0.
Search in Google Scholar Back to article
Alexander M. Nelson. Semidirect products of groups. Formalized Mathematics, 33(1): 65–83, 2025. doi:10.2478/forma-2025-0006.
Search in Google Scholar Back to article
Colin Rothgang, Artur Korniłowicz, and Florian Rabe. A new export of the Mizar Mathematical Library. In F. Kamareddine and C.S. Coen, editors, Intelligent Computer Mathematics (CICM 2021), volume 12833 of Lecture Notes in Artificial Intelligence, pages 205–210, 2021. ISBN 978-3-030-81097-9; 978-3-030-81096-2. doi:10.1007/978-3-030-81097-9_17.
Search in Google Scholar Back to article
Walter Rudin. Unique right inverses are two-sided. The American Mathematical Monthly, 92(7):489–490, 1985. doi:10.1080/00029890.1985.11971659.
Search in Google Scholar Back to article
Richard Schmoetten and Jacques D. Fleuriot. Constructing the Lie algebra of smooth vector fields on a Lie group in Isabelle/HOL. Journal of Automated Reasoning, 69(3):18, 2025. doi:10.1007/s10817-025-09724-x.
Search in Google Scholar Back to article
Christoph Schwarzweller. Finite fields. Formalized Mathematics, 32(1):289–302, 2024. doi:10.2478/forma-2024-0024.
Search in Google Scholar Back to article
Christoph Schwarzweller. Ring and field adjunctions, algebraic elements and minimal polynomials. Formalized Mathematics, 28(3):251–261, 2020. doi:10.2478/forma-2020-0022.
Search in Google Scholar Back to article
Christoph Schwarzweller and Agnieszka Rowińska-Schwarzweller. Some standard examples of vector spaces. Formalized Mathematics, 32(1):223–233, 2024. doi:10.2478/forma-2024-0019.
Search in Google Scholar Back to article
Joachim Schwermer. The general linear group over rings. In Reduction Theory and Arithmetic Groups, pages 46–69. Cambridge University Press, 2022. doi:10.1017/9781108937610.004.
Search in Google Scholar Back to article
Xiaopeng Yue, Xiquan Liang, and Zhongpin Sun. Some properties of some special matrices. Formalized Mathematics, 13(4):541–547, 2005.
Search in Google Scholar Back to article

Articles in this issue

DOI: https://doi.org/10.2478/forma-2026-0003 | Journal eISSN: 1898-9934 | Journal ISSN: 1426-2630

Journal RSS Feed

Language: English

Page range: 17 - 40

Submitted on: May 27, 2025

Accepted on: Sep 18, 2026

Published online: Oct 16, 2026

Published in print: Jun 1, 2026

Published by: University of Białystok

In partnership with: Paradigm Publishing Services

Keywords:

general linear group,

matrix ring,

group of units

MSC:

20H25,

16S50,

16U60,

68V20

Related subjects:

Computer sciences,

Artificial intelligence,

Computer sciences, other,

Mathematics,

Logic and set theory,

General mathematics

© 2026 Alexander M. Nelson, published by University of Białystok
This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 License.

Volume 34 (2026): Issue 1 (June 2026)