← all areas

Namespace IsAddCyclic 3 theorems

• Finite abelian p-group with socle of order ≤ p is cyclic IsAddCyclic.of_card_torsion_le_of_exponent_dvd_pow 0 below · cited by 7 · depth 6
• Abelian groups of squarefree order are cyclic IsAddCyclic.of_squarefree_natCard 0 below · cited by 1 · depth 13
• Non-zero ℓ-torsion in a cyclic group has ℓ-1 elements IsAddCyclic.ncard_setOf_nsmul_eq_zero_and_ne_zero_of_prime_dvd_card 0 below · cited by 1 · depth 35