Zulip Chat Archive

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

Kenny Lau (Dec 19 2018 at 14:40):

PR it lol

Andreas Swerdlow (Dec 19 2018 at 14:54):

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

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: Dec 20 2023 at 11:08 UTC