← all areas

Namespace Subgroup 20 theorems

— 19 · IsArithmetic 1

directly in Subgroup 19

• Index multiplicativity forces G = H₁H₂ Subgroup.exists_eq_mul_of_index_inf_eq 0 below · cited by 1 · depth 11
• Frobenius density modulo an open subgroup of Gal(ℚ̄/ℚ) Subgroup.exists_prime_isFrobeniusAt_conj_pow_mem_of_isOpen 22 below · cited by 6 · depth 11
• Frobenius density over ℚ, division form Subgroup.exists_prime_isFrobeniusAt_conj_pow_mem_conj_mem_of_isOpen 18 below · cited by 6 · depth 12
• Free double-coset count: #(Hbackslash M/K)·|K|=[M:H] Subgroup.card_orbitRelQuotient_mul_card_eq_index 0 below · cited by 2 · depth 15
• Exact fundamental domain for a discrete subgroup Subgroup.exists_exact_fundamental_domain_of_secondCountableTopology 0 below · cited by 3 · depth 17
• Existence of Artin induction coefficients on cyclic p'-subgroups Subgroup.exists_int_forall_finsum_ite_eq_one 0 below · cited by 1 · depth 18
• Wild–tame–unramified chain descends to intermediate normal pairs Subgroup.exists_wild_tame_unramified_chain_of_le 0 below · cited by 1 · depth 18
• Artin's counting identity at p-regular elements Subgroup.finsum_card_mul_card_fixedBy_quotient_eq_card 0 below · cited by 1 · depth 18
• Wild–tame–unramified chain with cyclic tame and top steps Subgroup.exists_wild_tame_cyclic_unramified_chain_of_le 0 below · cited by 1 · depth 21
• Index of K∩ gKg⁻¹ counts K-cosets in KgK Subgroup.relIndex_inf_map_conj_eq_natCard_setOf_exists_quotientMk_mul_eq 0 below · cited by 2 · depth 22
• Fibre degrees of a double coset degeneracy map sum to [K:K'] Subgroup.sum_fibre_doubleCoset_relIndex_inf_map_conj_eq_relIndex 0 below · cited by 2 · depth 22
• Harmonicity of forgetful maps between double coset spaces Subgroup.sum_fibre_doubleCoset_relIndex_inf_map_conj_eq_relIndex_of_le_inf 0 below · cited by 2 · depth 22
• Quotient by an involution under quadratic trace relations mod M Subgroup.card_quotient_zpowers_le_three_of_injective_of_sq_sub_mul_add_one_eq_zero 0 below · cited by 2 · depth 28
• Quotient H/⟨ c⟩ ≅ I from a surjection with index-matched cyclic kernel Subgroup.nonempty_quotient_zpowers_mulEquiv_of_forall_apply_mem_iff 0 below · cited by 1 · depth 29
• Normal torsion-free finite-index subgroup via the normal core Subgroup.exists_le_normal_subgroupOf_relIndex_ne_zero_torsionFree_of_relIndex_ne_zero 0 below · cited by 1 · depth 30
• Unique factorisation A=μ·{cⱼ}· H and sum re-indexing Subgroup.existsUnique_eq_mul_mul_and_finsum_mem_eq_sum_sum_finsum_mem_of_existsUnique_mul_inv_mem 0 below · cited by 2 · depth 33
• Exactly one coset cell contributes to a double sum Subgroup.sum_sum_mul_ite_inv_mul_mem_and_eq_of_pairwise_inv_mul_notMem 0 below · cited by 1 · depth 35
• Central commutators give a bimultiplicative alternating pairing Subgroup.commutatorElement_eq_and_mul_and_pow_of_forall_commutatorElement_mem_of_le_center 0 below · cited by 3 · depth 36
• Splitting a central extension over an exponent-2 subgroup Subgroup.exists_subgroup_injOn_map_eq_of_ker_le_center_of_comm 0 below · cited by 1 · depth 41

Subgroup.IsArithmetic 1

• A uniform integer period for all SL₂(ℤ)-conjugates Subgroup.IsArithmetic.exists_nat_mem_strictPeriods_conj 0 below · cited by 3 · depth 12