Theorems · Theorem · group theory

Finset.card_nsmul_quotient_add_nsmul_inter_addSubgroup_le

∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {H : AddSubgroup G}
  [inst_2 : DecidablePred fun x => x ∈ H] [inst_3 : H.Normal] {A : Finset G} {m n : ℕ},
  (Finset.image (⇑(QuotientAddGroup.mk' H)) (m • A)).card * {x ∈ n • A | x ∈ H}.card ≤ ((m + n) • A).card

Defined in

Mathlib.Geometry.Group.Growth.QuotientInter

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddGroupDecidableEqDecidablePredAddSubgroup.Normal