← all areas

Namespace Valued 9 theorems

• Adic completeness of the valuation ring of a complete valued field Valued.isAdicComplete_integer_span_singleton_of_forall_exists_pow_lt 0 below · cited by 8 · depth 18
• Adic continuity of ev from valuations of generators Valued.forall_exists_pow_le_comap_span_singleton_pow_of_eq_span 0 below · cited by 3 · depth 19
• Ultrametric Newton lemma: unimodular linear map plus small perturbation is onto Valued.exists_mulVec_add_eq_of_v_det_eq_one 0 below · cited by 2 · depth 24
• Finite-dimensional subspaces over a closed valued subfield are closed Valued.isClosed_submodule_of_finiteDimensional_of_isClosed_subfield 0 below · cited by 1 · depth 24
• Convergence of prod(1+fᵢ) in a complete valued field Valued.multipliable_one_add_of_tendsto_cofinite_zero 0 below · cited by 1 · depth 24
• Ultrametric product estimate with Lipschitz quadratic remainder Valued.v_prod_sub_one_sub_sum_sub_le_of_forall_v_sub_sub_mul_sub_le 0 below · cited by 2 · depth 24
• Valuation of an infinite product with finitely many non-unit factors Valued.v_tprod_eq_finsetProd_of_forall_not_mem_v_eq_one 0 below · cited by 2 · depth 24
• Generic centres make a partial-fraction matrix unimodular Valued.exists_forall_v_sub_eq_one_and_v_det_eq_one_of_v_sub_sum_div_lt_one 0 below · cited by 1 · depth 25
• A valuation takes finitely many values on a compact set avoiding 0 Valued.finite_image_v_of_isCompact_of_zero_notMem 0 below · cited by 2 · depth 33