## Stream: general

### Topic: isomorphisms

#### Kenny Lau (Dec 19 2018 at 08:10):

If I want to define ring_equiv and group_equiv and etc (I don't have any more examples at the moment), where should I put them?

#### Kenny Lau (Dec 19 2018 at 08:11):

or maybe should I not do it at all because either category_theory or parametricity will make this obsolete?

#### Andreas Swerdlow (Dec 19 2018 at 14:37):

https://github.com/leanprover-community/mathlib/blob/inner_product_spaces/ring_theory/ring_hom_isom_invo.lean
I made a start on ring isomorphisms here if that helps

PR it lol

Soon

#### Kenny Lau (Dec 19 2018 at 15:13):

you might want to see this: https://github.com/leanprover/mathlib/pull/533

#### Kenny Lau (Dec 19 2018 at 15:19):

don't use def for theorems

#### Kenny Lau (Dec 19 2018 at 15:54):

https://github.com/leanprover-community/mathlib/pull/12