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.
Jordan Normal Form
Cayley Hamilton theorem
All of Complex Analysis
- Cauchy Riemann equations
- Harmonic functions
- Cauchy Integral formula
- Laurent series
- Complex power series
- Residue theory
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 Cayley-Hamilton 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 Gin-ge Chen (Jan 11 2020 at 17:45):
Re: dihedral groups, there's this mathlib PR https://github.com/leanprover-community/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