mathlib3

297806e6 - feat(topology/homeomorph): sum_prod_distrib (#2870)

feat(topology/homeomorph): sum_prod_distrib (#2870) Also modify the `inv_fun` of `equiv.sum_prod_distrib` to have more useful definitional behavior. This also simplifies `measurable_equiv.sum_prod_distrib`.