Theorems · Theorem · number theory

IsApproximateSubgroup.pow_inter_pow_covBySMul_sq_inter_sq

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

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

Group