Ezra

On challenge 8, Lean complains that it doesn't know the word "group", so (poking through mathlib docs) we'd better import algebra.group.basic. This also puts mul_inv_rev into our list of completions,...

Power World 10 (Fermat's Last Theorem) is mostly pretty careful to frame it entirely in language we know: (a+1) instead of (n>0), etc. But it doesn't _quite_ finish the job:...