Zulip Chat Archive

Stream: mathlib4

Topic: Equidecomposability of two sets

Christian K (Mar 04 2024 at 17:12):

My first question is: Is there code in the Mathlib for the Equidecomposability of two sets in the Mathlib? I found nothing but I was wondering if i overlooked something.
And, if there isn't anything yet, I was wondering if it would make sense to open a PR with my definition of Equidecomposability?

Yaël Dillies (Mar 04 2024 at 17:21):

No we don't have equidecomposability. You are welcome to open a PR!

Christian K (Mar 04 2024 at 17:23):

Ok that is nice, I'll open one this evening

Christian K (Mar 04 2024 at 20:06):

Should I put it in an existing File or should I create a new one?

Last updated: May 02 2025 at 03:31 UTC