Zulip Chat Archive

Stream: maths

Topic: compulsory pure undergraduate maths that is not in Lean


view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Chris Hughes (Jan 11 2020 at 17:42):

I don't remember that happening.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 11 2020 at 17:43):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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