Tag Archives: M1F

The inverse of a bijection.

Constructing the inverse of a bijection in Lean can be tricky for beginners. Continue reading

Posted in Learning Lean, M1F | Tagged , | 6 Comments

M1F, Imperial undergraduates, and Lean

Abhimanyu Pallavi Sudhir, a current first year, has formalised the solutions to last year’s M1F final exam! Continue reading

Posted in M1F, undergrad maths | Tagged , , , | 1 Comment