← all areas

Namespace Padic 12 theorems

• Inertia fixes square roots of p-adic units, p odd Padic.forall_mem_inertiaSubgroupIn_apply_eq_of_sq_eq_of_nnnorm_eq_one 0 below · cited by 2 · depth 12
• Existence of ℂₚ with isometric Galois extensions Padic.exists_complete_algClosed_isometry_algebraicClosure 0 below · cited by 4 · depth 13
• Valuation divisible by p: a=(1+p)^r wᵖ in ℚₚ Padic.exists_eq_one_add_prime_pow_mul_pow_of_dvd_valuation 0 below · cited by 1 · depth 13
• #(ℚₚ^×/(ℚₚ^×)ᵖ) = p² for odd p Padic.natCard_units_quot_range_powMonoidHom_of_ne_two 8 below · cited by 2 · depth 14
• Index of p-th powers in ℚₚ^× is p² for odd p Padic.index_range_powMonoidHom_units_of_ne_two 7 below · cited by 1 · depth 15
• p-divisibility of exponents in pⁱ(1+p)^j=yᵖ over ℚₚ Padic.dvd_of_prime_zpow_mul_one_add_prime_zpow_eq_pow 2 below · cited by 1 · depth 16
• Generators of ℚₚ^× modulo p-th powers, p odd Padic.exists_eq_prime_pow_mul_one_add_prime_pow_mul_pow 3 below · cited by 1 · depth 16
• Isotropy of z²-ax²-by² over ℚ₂ for units a,b Padic.exists_ternary_isotropic_iff_of_norm_eq_one_two 0 below · cited by 4 · depth 18
• Ternary forms in p-adic units are isotropic, p odd Padic.exists_ternary_isotropic_of_norm_eq_one_of_ne_two 0 below · cited by 10 · depth 18
• Isotropy of z²-pax²-by² over ℚₚ, p odd Padic.exists_ternary_isotropic_prime_mul_iff_isSquare_of_ne_two 0 below · cited by 2 · depth 18
• Isotropy of z²-2ax²-by² over ℚ₂ for units a,b Padic.exists_ternary_isotropic_two_mul_iff_of_norm_eq_one 0 below · cited by 2 · depth 18
• Anticommuting endomorphisms make z²=ux²+vy² isotropic over ℚ_ℓ Padic.exists_ternary_isotropic_of_sq_eq_smul_of_anticommute 0 below · cited by 1 · depth 19