Formalization of James & Liebeck's "Representations and Characters of Groups"

Goal

Systematically formalize results from Gordon James and Martin Liebeck's Representations and Characters of Groups, Second Edition (2003).

Approach

• Follow the textbook linearly
• Use existing mathlib results where available (noted in comments)
• Formalize all major theorems and representative examples
• Skip or simplify some routine calculations where appropriate

Progress

Chapter 1: Groups and homomorphism

• Work in progress

Chapters 2-32

• Not yet started

Solutions to Exercises

• Not yet started

Mathlib Dependencies

• Will summarise key defintions/theorems used from mathlib as we progress

Departures from Textbook

• Any deviations from James & Liebeck will be documented here.

Notes for Lean Learners

• Common patterns used in the formalisation will be documented here.