This repository contains an ongoing formalization of the Artin-Wedderburn theorem in the proof assistant Lean 4.
Matevž Miščič, Maša Žaucer, Job Petrovčič
Information about the actual formalization is available at the project web pages:
JobPetrovcic/ArtinWedderburn
Folders and files
| Name | Name | Last commit date | ||
|---|---|---|---|---|