3 ms·
If nothing else it has pedagogical value, convincing yourself that the set and operations you established are the “same” as the ones you’re using for the rest o
by titanomachy 1y ago
If nothing else it has pedagogical value, convincing yourself that the set and operations you established are the “same” as the ones you’re using for the rest of the book.
- danabramov 1y agoI loved that from the pedagogical perspective personally. When I dreamed about this textbook getting formalized, I was worried about how unwieldy the formalization could become if it strayed too far from Mathlib — but also was worried about losing the self-contained-ness if it just used Mathlib. This is a nice compromise imo.