Theorems · Theorem · group theory

Finset.le_card_quotient_add_sq_inter_addSubgroup

∀ {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},
  -A = A → A.card ≤ (Finset.image (⇑(QuotientAddGroup.mk' H)) A).card * {x ∈ 2 • A | x ∈ H}.card

Defined in

Mathlib.Geometry.Group.Growth.QuotientInter

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddGroupDecidableEqDecidablePredAddSubgroup.Normal