← all areas

Namespace CommGroup 2 theorems

• Index of n-th powers in a finitely generated torsion-free abelian group CommGroup.index_range_powMonoidHom_eq_pow_finrank 0 below · cited by 1 · depth 19
• Symmetric cocycles on a finite abelian group split after adjoining roots CommGroup.exists_forall_monoidHom_exists_apply_eq_mul_inv_mul_inv_of_symm_of_cocycle 0 below · cited by 1 · depth 35