Namespace CharacterModule 2 theorems
- Character group of a finite abelian group has the same order
CharacterModule.natCard_eq_of_finite0 below · cited by 5 · depth 13 - Character counting: #(G^∨/bG^∨)=#G[b] for finitely generated b
CharacterModule.natCard_quotient_ideal_smul_top_eq_natCard_torsionBySet1 below · cited by 2 · depth 13