English
In a Z/pZ-module G, for a submodule H and any k with k ≤ |Subtype| and k ≠ 0, there exists H' ≤ H with |H'| ≤ k and k < p·|H'|.
Русский
В Z/pZ-модуляe G для субмодуля H и любого k с k ≤ |H| и k ≠ 0 существует H' ≤ H с |H'| ≤ k и k < p·|H'|.
LaTeX
$$$\\text{Nat.Prime } p \\rightarrow \\forall H:\\ Submodule(\\mathbb{Z}/p\\mathbb{Z})G,\\ k:\\mathbb{N},\\; k \\le |H| \\rightarrow k \\neq 0 \\rightarrow \\exists H' \\le H,\\; |H'| \\le k \\land k < p\\cdot |H'|$$$
Lean4
/-- In an elementary abelian `p`-group, every finite subgroup `H` contains a further subgroup of
cardinality between `k` and `p * k`, if `k ≤ |H|`. -/
theorem exists_submodule_subset_card_le (hp : p.Prime) [Module (ZMod p) G] (H : Submodule (ZMod p) G) {k : ℕ}
(hk : k ≤ Nat.card H) (h'k : k ≠ 0) : ∃ H' : Submodule (ZMod p) G, Nat.card H' ≤ k ∧ k < p * Nat.card H' ∧ H' ≤ H :=
by
obtain ⟨H'm, H'mHm, H'mk, kH'm⟩ :=
Sylow.exists_subgroup_le_card_le (H := AddSubgroup.toSubgroup ((AddSubgroup.toZModSubmodule _).symm H)) hp
isPGroup_multiplicative hk h'k
exact ⟨AddSubgroup.toZModSubmodule _ (AddSubgroup.toSubgroup.symm H'm), H'mk, kH'm, H'mHm⟩
