Commit 2024-12-10 17:35 7817ae82

View on Github →

feat: relation of covering by cosets (#19509) Define a predicate for a set to be covered by at most K cosets of another set. This is a fundamental relation to study in additive combinatorics. From GrowthInGroups (LeanCamCombi)

Estimated changes

added theorem CovBySMul.mono
added theorem CovBySMul.nonneg
added theorem CovBySMul.of_subset
added theorem CovBySMul.rfl
added theorem CovBySMul.subset
added theorem CovBySMul.subset_left
added theorem CovBySMul.subset_right
added theorem CovBySMul.trans
added def CovBySMul
added theorem covBySMul_zero