Zulip Chat Archive
Stream: maths
Topic: compulsory pure undergraduate maths that is not in Lean
Chris Hughes (Jan 11 2020 at 17:39):
@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 (Jan 11 2020 at 17:41):
Did we not knock up a proof of CayleyHamilton in that big summer project thing in 2018? It didn't make it into mathlib?
Chris Hughes (Jan 11 2020 at 17:42):
I don't remember that happening.
Kevin Buzzard (Jan 11 2020 at 17:42):
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 (Jan 11 2020 at 17:43):
Oh  maybe it was det(AB)=det(A)det(B) that we did in 2018
Bryan Ginge Chen (Jan 11 2020 at 17:45):
Re: dihedral groups, there's this mathlib PR https://github.com/leanprovercommunity/mathlib/pull/1076
Neil Strickland (Jan 11 2020 at 22:38):
I'm working on that PR and related things just now. I will update the PR in the next few days.
Kevin Buzzard (Jan 12 2020 at 00:13):
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 :)
Last updated: May 18 2021 at 06:15 UTC