mathlib3

cee5ddf3 - chore(topology/homeomorph): review, add `prod_punit`/`punit_prod` (#6180)

chore(topology/homeomorph): review, add `prod_punit`/`punit_prod` (#6180) * use `to_equiv := e` instead of `.. e` to have definitional equality `h.to_equiv = e`; * add some `@[simp]` lemmas; * add `homeomorph.prod_punit` and `homeomorph.punit_prod`; * generalize `unit.topological_space` to `punit.topological_space`.