Zulip Chat Archive

Stream: Is there code for X?

Topic: Equivalences between containers induced elementwise

Eric Wieser (Dec 17 2021 at 14:50):

Do we have any of the following?

  • α ≃ β → list α ≃ list β
  • α ≃ β → multiset α ≃ multiset β
  • α ≃ β → finset α ≃ finset β

Kevin Buzzard (Dec 17 2021 at 14:50):

Is there a tactic which does all these?

Eric Wieser (Dec 17 2021 at 14:51):

Probably more a metaprogram like to_additive

Eric Wieser (Dec 17 2021 at 14:53):

I think we might have docs#equiv_functor or similar, but it's not universe polymorphic so isn't as strong as the defs above would be

Floris van Doorn (Dec 17 2021 at 14:53):

There is docs#equiv.finset_congr

Eric Wieser (Dec 17 2021 at 16:54):

Well that's one out of three...

Yury G. Kudryashov (Dec 17 2021 at 17:31):

docs#equiv.list_equiv_of_equiv

Yury G. Kudryashov (Dec 17 2021 at 17:33):

And we don't have a version for multiset. Could you please add it as an add_equiv?

Kevin Buzzard (Dec 17 2021 at 17:34):

I read that as "add it with @[to_additive]" and I thought "but we don't have addtisets"

Yaël Dillies (Dec 17 2021 at 17:34):

Overadditivization :rofl:
Have a look at docs#add_salem_spencer.sum

Yaël Dillies (Dec 17 2021 at 17:34):

to_additive tricked me on that one.

Eric Wieser (Dec 17 2021 at 18:02):

@Huỳnh Trần Khanh, this is in the context of the α ≃ β → sym α n ≃ sym β n def I asked for in your stars and bars PR. It looks like equiv.sym_congr might be a better name than sym.map_equiv.

Eric Wieser (Dec 17 2021 at 18:03):

Are you happy to add equiv.multiset_congr : α ≃ β → multiset α ≃+ multiset β at the same time?

Last updated: Dec 20 2023 at 11:08 UTC