Theorems · Theorem · commutative algebra

ZModModule.exists_submodule_subset_card_le

∀ {p : ℕ} {G : Type u_5} [inst : AddCommGroup G],
  Nat.Prime p →
    ∀ [inst_1 : Module (ZMod p) G] (H : Submodule (ZMod p) G) {k : ℕ},
      k ≤ Nat.card ↥H → k ≠ 0 → ∃ H', Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H' ∧ H' ≤ H

In an elementary abelian p-group, every finite subgroup H contains a further subgroup of cardinality between k and p * k, if k ≤ |H|.

Defined in

Mathlib.Algebra.Module.ZMod

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommGroupModule