← all areas

Namespace ZMod 14 theorems

• A uniform family of surjections onto the groups Δ_q ZMod.exists_surjective_units_to_multiplicative_padic_family 0 below · cited by 3 · depth 10
• Cyclic subgroups of order n in (ℤ/n)² number ψ(n) ZMod.natCard_isAddCyclic_addSubgroup_prod_eq_dedekindPsi 3 below · cited by 3 · depth 13
• Counting τ-stable cyclic subgroups of order n in (ℤ/n)² ZMod.natCard_isAddCyclic_addSubgroup_prod_map_eq_nuThree 0 below · cited by 3 · depth 14
• Counting τ-stable cyclic subgroups of order n in (ℤ/n)² ZMod.natCard_isAddCyclic_addSubgroup_prod_map_eq_nuTwo 0 below · cited by 3 · depth 14
• Subgroup of (ℤ/p^{vₚ(q)+1})^× killed by q has order dividing q ZMod.natCard_dvd_of_forall_pow_eq_one_units_prime_pow 0 below · cited by 1 · depth 17
• Antisymmetry of the chord-crossing matrix on ℤ/2m ZMod.chordMatrix_transpose_eq_neg 0 below · cited by 1 · depth 18
• Partial zeta values as finite Fourier sums of Bernoulli values ZMod.tsum_intCast_pow_inv_eq_sum_bernoulliFun 0 below · cited by 1 · depth 19
• Invertibility of the kernel π²/sin² on (ℤ/N)^× ZMod.exists_sum_units_pi_sq_div_sin_sq_mul_eq 1 below · cited by 1 · depth 21
• No square root of -1 in ℤ/M for suitable odd M ZMod.not_exists_sq_add_one_eq_zero_of_not_two_dvd_of_exists_prime_dvd_mod_four_ne_one 1 below · cited by 1 · depth 28
• No root of x²+x+1 modulo M ZMod.not_exists_sq_add_self_add_one_eq_zero_of_not_three_dvd_of_exists_prime_dvd_mod_three_ne_one 1 below · cited by 1 · depth 28
• Prime divisors of M when x²+x+1≡ 0 (mod M) ZMod.prime_dvd_eq_three_or_mod_three_eq_one_of_sq_add_self_add_one_eq_zero 0 below · cited by 1 · depth 29
• Prime divisors of M admitting a square root of -1 ZMod.prime_dvd_eq_two_or_mod_four_eq_one_of_sq_add_one_eq_zero 0 below · cited by 1 · depth 29
• Heisenberg bicharacter ζ^{c(h)} on prodℤ/δᵢ and its dual ZMod.card_addMonoidHom_pi_eq_and_bichar_pow_val_of_isUnit_one_sub_pow 1 below · cited by 2 · depth 33
• Standard symplectic form on H(δ)× H(δ) ZMod.exists_addEquiv_prod_addMonoidHom_forall_apply_eq_sub_of_alternating_of_nondegenerate 5 below · cited by 1 · depth 33