Content
@
0 reply
0 recast
0 reaction
Agost Biro
@agostbiro
Did the solutions for the first batch of exercises: https://github.com/leanprover-community/mathematics_in_lean/commit/38575fb0c276f3ee8078f87f18dc3d694e715834 Most of them were pretty straightforward except for the last one (pictured) where I started in a different direction than what the authors assumed and needed the `sub_add_comm` theorem that hasn't been introduced yet. I couldn't find it by checking the docs/searching, so in the end I had to guess the name of the theorem which was a bit frustrating. Jumping to definition in a proof is magical though. (Repeating the left side in the calc section is something that I came up with for better alignment)
0 reply
0 recast
5 reactions
