General Linear Group over Arbitrary Rings
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.
- Broderick Arneson and Piotr Rudnicki. Primitive roots of unity and cyclotomic polynomials. Formalized Mathematics, 12(1):59–67, 2004.
- Broderick Arneson, Matthias Baaz, and Piotr Rudnicki. Witt’s proof of the Wedderburn theorem. Formalized Mathematics, 12(1):69–75, 2004.
- 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.
- Hyman Bass. K-theory and stable algebra. Publications Mathématiques de l’IHÉS, 22: 5–60, 1964. doi:10.1007/BF02684689.
- Nicolas Bourbaki. Elements of Mathematics. Algebra I. Chapters 1-3. Springer-Verlag, Berlin, Heidelberg, New York, London, Paris, Tokyo, 1989.
- Nicolas Bourbaki. Algebra: Chapter 8. Springer Nature, 2023.
- 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.
- 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.
- Francis E.A. Johnson. On the general linear group over polynomial rings. Mathematics, 14(6):942, 2026. doi:10.3390/math14060942.
- Niklas Krofta. Topological groups. Archive of Formal Proofs, August 2024. Formal proof development in Isabelle/HOL.
- Tsit-Yuen Lam. A First Course in Noncommutative Rings, volume 131 of Graduate Texts in Mathematics. Springer, New York, 2 edition, 2001.
- Oliver Nash. Engel’s theorem in Mathlib. Journal of Automated Reasoning, 67(2):18, 2023. doi:10.1007/s10817-023-09668-0.
- Alexander M. Nelson. Semidirect products of groups. Formalized Mathematics, 33(1): 65–83, 2025. doi:10.2478/forma-2025-0006.
- 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.
- Walter Rudin. Unique right inverses are two-sided. The American Mathematical Monthly, 92(7):489–490, 1985. doi:10.1080/00029890.1985.11971659.
- 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.
- Christoph Schwarzweller. Finite fields. Formalized Mathematics, 32(1):289–302, 2024. doi:10.2478/forma-2024-0024.
- Christoph Schwarzweller. Ring and field adjunctions, algebraic elements and minimal polynomials. Formalized Mathematics, 28(3):251–261, 2020. doi:10.2478/forma-2020-0022.
- 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.
- 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.
- Xiaopeng Yue, Xiquan Liang, and Zhongpin Sun. Some properties of some special matrices. Formalized Mathematics, 13(4):541–547, 2005.
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:
Related subjects:
© 2026 Alexander M. Nelson, published by University of Białystok
This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 License.