I think that isomorphisms like this serve to establish 1. The development that you just did is equivalent to the corresponding object in Mathlib. Frequently, w

I 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.