Card triple (2,7,8) of units covers Z/15Z

Proved

ShaoThreeUnits.cover_row_2_7_8

by hitme development · Sep 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

additive-combinatoricsnumber-theory

Let $U$ be the unit group of $\\mathbb{Z}/15\\mathbb{Z}$ , the eight residues $1,2,4,7,8,11,13,14$ . If the card triple is $(2,7,8)$ with subsets of $U$ , then any eight-element set equals $U$ and the sumset equals all of $\\mathbb{Z}/15\\mathbb{Z}$ . This is the $(2,7,8)$ card row of Shao Lemma 2.3 (arXiv:1206.6139).

Formalization Note. The Lean statement is ShaoThreeUnits.cover_row_2_7_8.

Preamble

import Mathlib
open Finset
open scoped Pointwise

Formal statement

namespace ShaoThreeUnits
theorem cover_row_2_7_8 (A B C : Finset (ZMod 15))
    (hA : A ⊆ ({1, 2, 4, 7, 8, 11, 13, 14} : Finset (ZMod 15)) ∧ A.card = 2)
    (hB : B ⊆ ({1, 2, 4, 7, 8, 11, 13, 14} : Finset (ZMod 15)) ∧ B.card = 7)
    (hC : C ⊆ ({1, 2, 4, 7, 8, 11, 13, 14} : Finset (ZMod 15)) ∧ C.card = 8) :
    (A + B + C : Finset (ZMod 15)) = univ := by sorry
end ShaoThreeUnits

Source

Shao, Three units of Z/15Z, arXiv:1206.6139, Lemma 2.3, card triple (2,7,8)

View graph