Namespace AddCommGroup 22 theorems
- Groups with n-torsion (ℤ/n)² have ψ(n) cyclic subgroups of order n
AddCommGroup.natCard_isAddCyclic_addSubgroup_eq_dedekindPsi_of_addEquiv_torsionBy4 below · cited by 9 · depth 12 - #A[d]=d² for all d∣ n forces A[n]≅(ℤ/n)²
AddCommGroup.nonempty_zmod_prod_addEquiv_torsionBy_of_card_torsionBy_eq_sq0 below · cited by 7 · depth 12 - Counting σ-stable cyclic n-subgroups: the count is ν₃(n)
AddCommGroup.natCard_isAddCyclic_addSubgroup_map_eq_of_sq_add_self_add_id_eq_zero_eq_nuThree1 below · cited by 5 · depth 13 - σ-stable cyclic subgroups of order n number ν₂(n)
AddCommGroup.natCard_isAddCyclic_addSubgroup_map_eq_of_sq_eq_neg_one_eq_nuTwo1 below · cited by 3 · depth 13 - Bound on A[ℓ] from growth of τ^{ℓ^k}-fixed points
AddCommGroup.finite_and_natCard_torsionBy_le_of_natCard_fixed_primaryComponent_le_of_divisible0 below · cited by 1 · depth 17 - ℓ-power torsion from fixed-point counts of an endomorphism
AddCommGroup.natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent0 below · cited by 1 · depth 17 - Levelwise torsion counts give a free ℤ/ℓ^m-module of rank r
AddCommGroup.nonempty_basis_zmod_pow_of_card_torsionBy2 below · cited by 3 · depth 20 - Lifting bases of M[ℓ^m] to bases of M[ℓ^{m+1}]
AddCommGroup.exists_basis_smul_eq_of_card_torsionBy1 below · cited by 1 · depth 21 - M-torsion free of rank one over ℤ[β]/M and ℤ[α]/M
AddCommGroup.exists_torsionBy_coords_of_dicyclic_relations0 below · cited by 2 · depth 21 - ℓ-primary kernel orders of G(T) from resultants
AddCommGroup.natCard_primaryComponent_ker_aeval_of_forall_natCard_ker_aeval_eq_natAbs_resultant0 below · cited by 1 · depth 21 - Cyclic basis (v,σ v) of the n-torsion under a non-scalar endomorphism
AddCommGroup.exists_addEquiv_prod_torsionBy_apply_eq_of_forall_exists_ne_smul0 below · cited by 3 · depth 22 - Divisibility of ℓ-power torsion from exact torsion counts
AddCommGroup.exists_mem_torsionBy_smul_eq_of_card_torsionBy0 below · cited by 2 · depth 22 - Order-M points modulo ± H counted by an index
AddCommGroup.natCard_torsionOrbit_gammaH_eq_index2 below · cited by 5 · depth 22 - Polynomial along every progression implies polynomial function
AddCommGroup.exists_mvPolynomial_totalDegree_le_eval_eq_of_forall_exists_polynomial_zsmul_add0 below · cited by 3 · depth 25 - Cube identity forces quadratic behaviour along lines
AddCommGroup.apply_zsmul_add_eq_of_forall_cube0 below · cited by 2 · depth 26 - Finitely generated saturations from a separating homogeneous degree
AddCommGroup.exists_fg_saturation_of_isHomogeneous_degree0 below · cited by 1 · depth 29 - Finite freeness from finitely generated saturations and an n-divisible kernel
AddCommGroup.moduleFinite_and_free_of_fg_saturation_of_ker_le_nsmul0 below · cited by 1 · depth 29 - Recognising A[n] as (ℤ/n)^r from torsion counts
AddCommGroup.nonempty_pi_zmod_addEquiv_torsionBy_of_card_torsionBy_eq_pow3 below · cited by 1 · depth 33 - Counting homomorphisms into a cyclic group killing X
AddCommGroup.natCard_addMonoidHom_eq_of_isAddCyclic0 below · cited by 1 · depth 34 - Multiplicativity of N-torsion cardinality in a product
AddCommGroup.natCard_torsionBy_prod_eq_mul0 below · cited by 1 · depth 35 - Equal N-torsion counts force isomorphism of finite abelian groups
AddCommGroup.nonempty_addEquiv_of_forall_natCard_torsionBy_eq0 below · cited by 1 · depth 35 - A finite abelian group killed by d is isomorphic to Hom(L,ℤ/d)
AddCommGroup.nonempty_addMonoidHom_zmod_addEquiv_of_forall_nsmul_eq_zero0 below · cited by 1 · depth 35