← all areas

Namespace AddSubgroup 17 theorems

• Inertia-stable cyclic subgroup absorbed by inertial displacement subgroup AddSubgroup.eq_atP_filtration_of_cyclic_stable_inertia_nontrivial 0 below · cited by 1 · depth 6
• Tower step for Galois-stable cyclic p-power subgroups AddSubgroup.exists_towerStep_of_extVanishingCts 2 below · cited by 1 · depth 6
• Global triviality of p^m-torsion displacements from inertia AddSubgroup.galois_trivial_quotient_of_inertia_absorbing 4 below · cited by 1 · depth 6
• Cyclic σ-stable p^m-subgroup with non-±1 scalar is the toric subgroup AddSubgroup.inZeroComponentAt_of_cyclic_stable_scalar_dichotomy 1 below · cited by 1 · depth 6
• Zero-component p^m-torsion is contained in K AddSubgroup.mem_of_torsion_inZeroComponentAt_of_forall_not_inZeroComponentAt_sub 1 below · cited by 1 · depth 6
• Subgroups of finitely generated abelian groups are finitely generated AddSubgroup.addGroup_fg_of_le_of_addGroup_fg 0 below · cited by 3 · depth 9
• Admissible filtration with steps of prime order q AddSubgroup.exists_chain_card_quotient_eq_forall_sub_mem_or_sub_smul_mem 3 below · cited by 1 · depth 12
• Nonzero divisible subgroup from a coherent p-power torsion tower AddSubgroup.closure_range_divisible_of_prime_tower 0 below · cited by 2 · depth 17
• Bounded index forces C! K ⊆ H AddSubgroup.factorial_nsmul_mem_of_le_of_natCard_le_mul 0 below · cited by 1 · depth 23
• Adapted coordinates for a discrete subgroup of a real vector space AddSubgroup.exists_continuousLinearEquiv_prod_mem_iff_of_discreteTopology 0 below · cited by 1 · depth 29
• Equal-order points in one cyclic subgroup differ by a unit of ℤ/ℓ AddSubgroup.exists_units_zmod_val_smul_eq_of_addOrderOf_eq_of_mem_zmultiples 0 below · cited by 2 · depth 29
• Unipotent splitting of an 𝒪-stable subgroup of D² AddSubgroup.exists_forall_mem_iff_single_sub_mul_mem_of_sum_mul_eq_one 0 below · cited by 1 · depth 31
• Double annihilator of a subgroup under a non-degenerate pairing AddSubgroup.mem_of_forall_pairing_annihilator_eq_one_of_nondegenerate 0 below · cited by 3 · depth 31
• Counting C-fixed finite subgroups: #Y=p^{dim_Kspan_K Y} AddSubgroup.natCard_eq_pow_finrank_span_of_forall_apply_eq_self_of_map_pow_smul 1 below · cited by 1 · depth 31
• Uniform bound for product weights over a discrete subgroup AddSubgroup.exists_forall_sum_prod_inv_one_add_abs_sq_le_of_discreteTopology 0 below · cited by 1 · depth 33
• Discrete subgroups of ℝ^r × ℤᶜ meet boxes finitely AddSubgroup.finite_setOf_mem_forall_abs_le_snd_eq_of_discreteTopology 0 below · cited by 2 · depth 33
• Isotropic subgroups of complementary order are mutual annihilators AddSubgroup.forall_mem_of_forall_pairing_eq_one_of_natCard_mul_eq 1 below · cited by 1 · depth 34