Documentation

ClassificationOfSubgroups.Ch6_MaximalAbelianSubgroupClassEquation.S1_ElementaryAbelian

structure ElementaryAbelian (p : ) (G : Type u_1) [Group G] extends Subgroup G :
Type u_1
Instances For
    def IsElementaryAbelian {G : Type u_1} [Group G] (p : ) (H : Subgroup G) :
    Equations
    Instances For
      theorem IsElementaryAbelian.dvd_card {G : Type u_1} [Group G] (p : ) (H : Subgroup G) [Finite H] (hH : IsElementaryAbelian p H) (bot_lt_H : < H) :
      p Nat.card H
      theorem IsElementaryAbelian.primeFac_eq {G : Type u_1} [Group G] (p : ) (hp : Nat.Prime p) (H : Subgroup G) [Finite H] (hH : IsElementaryAbelian p H) (bot_lt_H : < H) :
      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) :