Zulip Chat Archive

Stream: general

Topic: isomorphisms


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Dec 19 2018 at 14:40):

PR it lol

view this post on Zulip Andreas Swerdlow (Dec 19 2018 at 14:54):

Soon

view this post on Zulip Kenny Lau (Dec 19 2018 at 15:13):

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

view this post on Zulip Kenny Lau (Dec 19 2018 at 15:19):

don't use def for theorems

view this post on Zulip Kenny Lau (Dec 19 2018 at 15:54):

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

view this post on Zulip Andreas Swerdlow (Dec 19 2018 at 18:28):

Is it worth adding the "lemmas" about ring_equiv from https://github.com/leanprover-community/mathlib/blob/inner_product_spaces/ring_theory/ring_hom_isom_invo.lean into your PR?


Last updated: May 10 2021 at 00:31 UTC