fundamental_domain): a large set contains 2 pts of the same orbit (#17293)

Commit

3 years ago

feat(measure_theory/group/fundamental_domain): a large set contains 2 pts of the same orbit (#17293) Motivated by #2819

Author

urkud

Parents