compulsory pure undergraduate maths that is not in Lean

Stream: maths

[Chris Hughes]

@Freek Wiedijk asked me for a list of compulsory undergraduate pure maths at Imperial College that is not yet in Lean. Compulsory pure modules comprise about half of the first two years at Imperial. This is the list in case anyone else is interested.

Generalised Eigenspaces
Jordan Normal Form
Cayley Hamilton theorem
Dihedral Groups
All of Complex Analysis

• Cauchy Riemann equations
• Harmonic functions
• Cauchy Integral formula
• Laurent series
• Complex power series
• Residue theory

• Conformal mappings
  Real analysis

• Fundamental theorem of calculus

• Interchanging limits and derivative
• Symmetry of mixed partial derivatives
• Taylor’s theorem (at higher order)
• Green’s theorem

[Kevin Buzzard]

Did we not knock up a proof of Cayley-Hamilton in that big summer project thing in 2018? It didn't make it into mathlib?

[Chris Hughes]

I don't remember that happening.

[Kevin Buzzard]

We definitely once knocked up a theory of dihedral groups at Xena because I remember about six people working on it at once in CoCalc ;-) At some point someone changed the definition and all the proofs instantly broke, and then lots of people all started fixing different ones at once :-) But for sure that didn't make it into mathlib.

[Kevin Buzzard]

Oh -- maybe it was det(AB)=det(A)det(B) that we did in 2018

[Bryan Gin-ge Chen]

Re: dihedral groups, there's this mathlib PR https://github.com/leanprover-community/mathlib/pull/1076

[Neil Strickland]

I'm working on that PR and related things just now. I will update the PR in the next few days.

[Kevin Buzzard]

When I was lecturing 2nd year group theory I would usually state but not prove the structure theorem for finitely generated abelian groups. Both that and Jordan Normal Form follow from the structure theorem for finely generated abelian groups, which was originally supposed to be @Amelia Livingston 's summer project but then we started talking about monoids and the rest is history :-)