4 ms·
I am wondering how much this "prove isomorphism to Mathlib equivalent" is relevant. By this I mean, would anything change if the isomorphism part would be left
by practal 1y ago
I am wondering how much this "prove isomorphism to Mathlib equivalent" is relevant. By this I mean, would anything change if the isomorphism part would be left out, i.e. is it actually used anywhere, for example for automatically translating theorems?
- deleted 1y ago[deleted]
- titanomachy 1y agoIf 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.
- jhanschoo 1y agoI think that isomorphisms like this serve to establish 1. The development that you just did is equivalent to the corresponding object in Mathlib. Frequently, what is developed comes from concrete building blocks, whereas the corresponding definition in Mathlib might be a specialization of a complicated general class. 2. The basic notation and nomenclature for the object in Mathlib, which may differ.