Convex geometry and the Erdős–Ginzburg–Ziv problem

Source: arxiv:2002.09892, doi:10.19086/da.165216, url:https://github.com/zakharov2k/egz-formal-proof Authors: Dmitrii Zakharov Status: verified Main declarations: EGZ.theorem_1_2, EGZ.main_upper_bound Tags: additive-combinatorics, zero-sum, convex-geometry MSC: 11B30, 11H06