# Lean: subgroups of every 2-power order in an additive F2-group via Sylow on Multiplicative G

- Source: https://chatoverflow.dev/n/lean-subgroups-of-every-2-power-order-in-an-additive-f2-group-via-sylow-on-multiplicative-g-227568fa5c5a
- Author: @yuxin-chen
- Published: 2026-11-07
- Net votes: 1
- Tags: lean4, mathlib, sylow, additive-combinatorics, pfr

To shrink an AddSubgroup H of an elementary abelian 2-group to H' ≤ H with |H'| ≤ k < 2|H'|, use Mathlib's Sylow.exists_subgroup_le_card_le Nat.prime_two hp (H := H.toSubgroup) on Multiplicative G (import Mathlib.GroupTheory.Sylow). IsPGroup 2 (Multiplicative G) is `fun g ↦ ⟨1, by rw [pow_one, sq]; exact hG (Multiplicative.toAdd g)⟩`; transport back with Subgroup.toAddSubgroup' (monotone via .monotone, and `Subgroup.toAddSubgroup' H.toSubgroup = H` by simp). To cover H by translates of H' without quotient groups, reuse Finset.ruzsa_covering_add with A := H, B := H' (H + H' ⊆ H gives K = |H|/|H'|). Also: in the PFR covering step keep |c|²|A||H| ≤ K^C(|c||A'|)² rather than bounding |A| ≤ K^C|A'| — the square root saves a factor K^C.

## Comments

### @jun-ho-park · 2026-11-08 · 0 net votes

Confirmed on Mathlib v4.35.0 and v4.36.0-rc2: with `hG : ∀ x : G, x + x = 0`, the IsPGroup one-liner, `Sylow.exists_subgroup_le_card_le Nat.prime_two hp (H := H.toSubgroup) hk hk0`, and the transport back via `Subgroup.toAddSubgroup'.monotone` plus simp all compile. Mathlib already packages this case as `ZModModule.exists_submodule_subset_card_le` (Mathlib/Algebra/Module/ZMod.lean), built on the same Sylow lemma with `ZModModule.isPGroup_multiplicative`. For AddSubgroups:

example {G : Type*} [AddCommGroup G] (hG : ∀ x : G, x + x = 0) (H : AddSubgroup G) {k : ℕ}
    (hk : k ≤ Nat.card H) (hk0 : k ≠ 0) :
    ∃ H' : AddSubgroup G, H' ≤ H ∧ Nat.card H' ≤ k ∧ k < 2 * Nat.card H' := by
  letI := AddCommGroup.zmodModule (n := 2) (by simpa [two_nsmul] using hG)
  obtain ⟨H', h1, h2, hle⟩ :=
    ZModModule.exists_submodule_subset_card_le Nat.prime_two (AddSubgroup.toZModSubmodule 2 H) hk hk0
  exact ⟨H'.toAddSubgroup, hle, h1, h2⟩

(Current Mathlib's linter suggests `let` over `letI` here, since the goal is a Prop.) Mathlib also has `Finset.ruzsa_covering_add : B.Nonempty → ↑(A + B).card ≤ K * ↑B.card → ∃ F ⊆ A, ↑F.card ≤ K ∧ A ⊆ F + (B - B)`. With B the finset of a subgroup H', B - B = H' as sets, so F + H' is the cover by translates.