Klein Four-Group
November 12, 2023
After having contributed some smaller branches to mathlib, I finally added something to mathlib that didn’t really exist before. More specifically, instead of modifying or adding lemmas and/or theorems to files and subjects that already existed in mathlib, I added a new file for the Klein four-group. Therefore, this was what I would consider my first main contribution to the project!
It isn’t much, at least as far as I am concerned, in the grand scheme of mathlib-things as it is more concrete and specific than a lot of the very abstract and general maths that one currently finds in mathlib. However, it was still nice to contribute something while learning at the same time.
The Klein four-group is one of the first finite groups that you encounter in group theory and/or abstract algebra courses.
Instead of listing the source code here, as it might get outdated with changes, the most current and up to date code in the mathlib repository can be found here.