Theorems · Theorem · number theory

IsApproximateAddSubgroup.nsmul_inter_nsmul_covByVAdd_sq_inter_sq

∀ {G : Type u_1} [inst : AddGroup G] {A B : Set G} {K L : ℝ} {m n : ℕ},
  IsApproximateAddSubgroup K A →
    IsApproximateAddSubgroup L B →
      2 ≤ m → 2 ≤ n → CovByVAdd G (K ^ (m - 1) * L ^ (n - 1)) (m • A ∩ n • B) (2 • A ∩ 2 • B)

Defined in

Mathlib.Combinatorics.Additive.ApproximateSubgroup

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddGroup