- is_comm : self.IsCommutative
- orderOf_eq (h : ↥self.toSubgroup) : h ≠ 1 → orderOf h = p
Instances For
Equations
- IsElementaryAbelian p H = (H.IsCommutative ∧ ∀ (h : ↥H), h ≠ 1 → orderOf h = p)
Instances For
theorem
IsElementaryAbelian.IsPGroup
{G : Type u_1}
[Group G]
(p : ℕ)
(hp : Nat.Prime p)
(H : Subgroup G)
[Finite ↥H]
(hH : IsElementaryAbelian p H)
(bot_lt_H : ⊥ < H)
:
_root_.IsPGroup p ↥H
theorem
IsElementaryAbelian.IsElementaryAbelian_subgroupOf
{G : Type u_1}
[Group G]
(H K : Subgroup G)
{p : ℕ}
[Fact (Nat.Prime p)]
(hH : IsElementaryAbelian p H)
:
IsElementaryAbelian p (H.subgroupOf K)