← all areas

Namespace AbsoluteValue 3 theorems

— 1 · Completion 2

directly in AbsoluteValue 1

• Artin–Whaples weak approximation for inequivalent absolute values AbsoluteValue.exists_forall_sub_lt_of_pairwise_not_isEquiv 0 below · cited by 1 · depth 16

AbsoluteValue.Completion 2

• Completion at a non-archimedean absolute value is ultrametric AbsoluteValue.Completion.isUltrametricDist_of_isNonarchimedean 0 below · cited by 1 · depth 18
• Completion of an absolute value: isometry and nontriviality of the norm AbsoluteValue.Completion.norm_coe_and_exists_one_lt_norm 0 below · cited by 1 · depth 18