Theorems · Definition · number theory

CovBySMul

(M : Type u_1) → {X : Type u_3} → [inst : Monoid M] → [MulAction M X] → ℝ → Set X → Set X → Prop

Predicate for a set A to be covered by at most K cosets of another set B under the action by the monoid M.

Defined in

Mathlib.Combinatorics.Additive.CovBySMul

Cited by

11 results in Mathlib

Foundations

Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MonoidMulAction