← all areas

Namespace PadicInt 26 theorems

— 22 · KummerCarrier 4

directly in PadicInt 22

• Kummer Hopf algebra witness with upper-triangular Galois action PadicInt.exists_finiteFlat_kummerHopf_withConv_equiv_of_nnnorm_eq_one 5 below · cited by 4 · depth 13
• Kummer Hopf algebra over ℤₚ with polynomial point evaluations PadicInt.exists_finiteFlat_kummerHopf_withConv_aeval 4 below · cited by 1 · depth 14
• Unramified degree-n étale ℤₚ-algebra with ℤ/n-torsor of points PadicInt.exists_etale_algebra_algHom_equiv_zmod 21 below · cited by 1 · depth 16
• Index of f(T) equals p^{v(det f)} for ℤₚ-modules PadicInt.natCard_quotient_range_eq_pow_valuation_det 0 below · cited by 2 · depth 16
• (1+p)^j a p-th power in ℤₚ forces p ∣ j PadicInt.dvd_of_one_add_prime_pow_eq_pow 1 below · cited by 1 · depth 17
• Units of ℤₚ as (1+p)^j zᵖ, p odd PadicInt.exists_eq_one_add_prime_pow_mul_pow 2 below · cited by 1 · depth 17
• ℚ̄ₚ-points of a module-finite ℤₚ-algebra lie in one finite extension PadicInt.exists_intermediateField_finiteDimensional_forall_algHom_apply_mem 0 below · cited by 1 · depth 17
• Units congruent to 1 mod p² are p-th powers of principal units PadicInt.exists_pow_eq_of_toZModPow_two_eq_one 1 below · cited by 1 · depth 18
• Ring homomorphism ℤₚ → S for I-adically complete S with p ∈ I PadicInt.nonempty_ringHom_of_isAdicComplete_of_natCast_mem 0 below · cited by 1 · depth 18
• p-th powers of principal units lie in 1+p²ℤₚ PadicInt.toZModPow_two_pow_eq_one_of_toZMod_eq_one 0 below · cited by 1 · depth 18
• Units of ℤₚ: p-th powers mod p³ lift PadicInt.exists_pow_eq_of_exists_pow_eq_toZModPow_three 0 below · cited by 1 · depth 19
• Nakayama glue: inertia acts by χ on corner displacements PadicInt.apply_sub_eq_smul_sub_of_idempotent_of_forall_sub_mem_of_forall_exists_pow_sub_smul 0 below · cited by 1 · depth 25
• Ring of integers of a finite extension of ℚₚ PadicInt.exists_completeDVR_finiteResidueField_isFractionRing_of_finiteDimensional 5 below · cited by 1 · depth 25
• Integral orthogonality: p^k v ∈ T^t+T^o PadicInt.exists_pow_smul_mem_sup_of_forall_bilinForm_apply_eq_zero 1 below · cited by 1 · depth 26
• Unramified quadratic norm form represents every p-adic unit PadicInt.exists_sq_add_mul_add_mul_sq_eq_of_isUnit_of_forall_ne_zero 0 below · cited by 1 · depth 28
• Existence of the completed maximal unramified extension of ℤ_q PadicInt.exists_isAdicComplete_isMaximal_span_natCast_and_frobenius_sub_pow_mem 0 below · cited by 2 · depth 30
• Common mod-p eigenvectors of unipotent operators number √#π(P) PadicInt.ncard_setOf_forall_apply_eq_nsmul_sq_eq_card_range_of_forall_sub_mem_iInf_ker 0 below · cited by 1 · depth 30
• Similitude eigenlattice is Lagrangian: half the rank PadicInt.two_mul_finrank_iInf_ker_eq_finrank_of_isBaseChange_of_bilinForm_similitude 1 below · cited by 1 · depth 30
• Uniqueness of ring maps ℤₚ → B when p is nilpotent PadicInt.ringHom_eq_ringHom_of_isNilpotent 0 below · cited by 5 · depth 33
• Additive maps between free ℤₚ-modules are ℤₚ-linear PadicInt.addMonoidHom_map_smul_of_free 0 below · cited by 8 · depth 35
• Uniform depth at which an injective additive map detects p-divisibility PadicInt.exists_forall_apply_eq_pow_smul_imp_exists_eq_smul_of_injective 1 below · cited by 1 · depth 36
• Injective additive endomorphism of ℤₚⁿ contains p^Nℤₚⁿ PadicInt.exists_forall_exists_apply_eq_pow_smul_of_injective 1 below · cited by 1 · depth 39

PadicInt.KummerCarrier 4

• Coalgebra axioms and cocommutativity for the Kummer carrier PadicInt.KummerCarrier.bialgebra_axioms 1 below · cited by 1 · depth 15
• Evaluation maps: bijective convolution homomorphism (ℤ/p)²→ points PadicInt.KummerCarrier.evalAt_bijective_convHom 0 below · cited by 1 · depth 15
• Existence of an antipode on the Kummer carrier PadicInt.KummerCarrier.exists_antipode 0 below · cited by 1 · depth 15
• Coassociativity of the Kummer carrier comultiplication PadicInt.KummerCarrier.comul_coassoc 0 below · cited by 1 · depth 16