Documentation Verification Report

Valuation

📁 Source: Mathlib/RingTheory/HahnSeries/Valuation.lean

Statistics

Metric	Count
Definitions `addVal`, `Valuation`, `Valuation`	3
Theorems `addVal_apply`, `addVal_apply_of_ne`, `addVal_le_of_coeff_ne_zero`	3
Total	6

HahnSeries

Definitions

Name	Category	Theorems
`addVal` 📖	CompOp	3 math math: `addVal_le_of_coeff_ne_zero`, `addVal_apply_of_ne`, `addVal_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addVal_apply` 📖	mathematical	—	`DFunLike.coe` `AddValuation` `HahnSeries` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRing` `AddCancelCommMonoid.toAddCommMonoid` `WithTop` `WithTop.linearOrderedAddCommMonoidWithTop` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `PartialOrder.toPreorder` `AddValuation.instFunLike` `addVal` `orderTop`	—	`AddValuation.of_apply`
`addVal_apply_of_ne` 📖	mathematical	—	`DFunLike.coe` `AddValuation` `HahnSeries` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRing` `AddCancelCommMonoid.toAddCommMonoid` `WithTop` `WithTop.linearOrderedAddCommMonoidWithTop` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `PartialOrder.toPreorder` `AddValuation.instFunLike` `addVal` `WithTop.some` `order` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `addVal_apply` `order_eq_orderTop_of_ne_zero`
`addVal_le_of_coeff_ne_zero` 📖	mathematical	—	`WithTop` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `AddValuation` `HahnSeries` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRing` `AddCancelCommMonoid.toAddCommMonoid` `WithTop.linearOrderedAddCommMonoidWithTop` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `AddValuation.instFunLike` `addVal` `WithTop.some`	—	`orderTop_le_of_coeff_ne_zero`

Sat

Definitions

Name	Category	Theorems
`Valuation` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`Valuation` 📖	CompData	505 math math: `Valuation.mem_nhds_zero_iff`, `Valued.continuous_extension`, `Valued.isOpen_closedball`, `Valuation.IsTrivialOn.valuation_algebraMap_le_one`, `Irreducible.maximalIdeal_eq_setOf_le_v_coe`, `Valuation.inversion_estimate'`, `WithVal.valued_toVal`, `ValuationSubring.valuation_lt_one_iff`, `Valuation.leSubmodule_v_le_of_mem`, `Valuation.FiniteField.algebraMap_le_one`, `Valuation.FiniteField.algebraMap_eq_one`, `WithVal.valueGroupOrderIso₀_symm_apply`, `Valuation.HasExtension.val_map_le_iff`, `Valuation.isEquiv_iff_val_sub_one_lt_one`, `Valuation.one_apply_lt_one_iff`, `Valuation.isClopen_closedBall`, `Valuation.mem_maximalIdeal_iff`, `Valuation.val_mrange_zero`, `Valuation.mem_leSubmodule_iff`, `Valuation.map_one_add_of_lt`, `Valuation.mem_supp_iff`, `Padic.withValUniformEquiv_norm_le_one_iff`, `Valued.toNormedField.norm_le_one_iff`, `Rat.padicValuation_cast`, `Valued.extension_extends`, `WithVal.valueGroup_eq`, `Valued.valuedCompletion_surjective_iff`, `ValuativeRel.valuation_eq_zero_iff`, `ValuationSubring.valuation_le_iff`, `IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff_mem_primeCompl`, `PadicComplex.valuation_extends`, `Valuation.IsRankOneDiscrete.exists_generator_lt_one'`, `WeierstrassCurve.HasAdditiveReduction.badReduction`, `RatFunc.exists_zpow_uniformizingPolynomial`, `Valuation.IsTrivialOn.eq_one`, `Valuation.Integers.one_of_isUnit'`, `Valuation.mem_ltIdeal_iff`, `Valuation.toFun_eq_coe`, `Valuation.val_le_one_or_val_inv_lt_one`, `NumberField.FinitePlace.norm_def'`, `WithVal.valueGroupOrderIso₀_restrict`, `IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers`, `FunctionField.inftyValuation.X_inv`, `WithVal.apply_ofVal`, `Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective`, `Int.padicValuation_lt_one_iff`, `Valuation.map_add_eq_of_lt_right`, `IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg`, `Valuation.IsRankOneDiscrete.generator_mem_valueGroup`, `IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap`, `WithVal.valueGroupOrderIso₀_apply`, `Valuation.Integers.isPrincipal_iff_exists_isGreatest`, `NumberField.HeightOneSpectrum.NumberField.toNNReal_valued_eq_adicAbv`, `LaurentSeries.valuation_le_iff_coeff_lt_eq_zero`, `LaurentSeries.valuation_single_zpow`, `RatFunc.irreducible_min_polynomial_valuation_lt_one_and_ne_zero`, `Valued.toUniformSpace_eq`, `IsDedekindDomain.HeightOneSpectrum.intValuation_le_one`, `ValuationSubring.ofPrime_valuation_eq_one_iff_mem_primeCompl`, `Valuation.instNontrivialSubtypeUnitsMemSubmonoidValueMonoidOfIsNontrivial`, `WeierstrassCurve.valuation_Δ_aux_eq_of_isIntegral`, `ValuationSubring.valuation_unit`, `NumberField.HeightOneSpectrum.rankOne_hom'_def`, `ArchimedeanClass.FiniteResidueField.mk_eq_zero`, `Valuation.Compatible.srel_iff_lt`, `WithVal.valueGroupEquiv_symm_apply`, `Valuation.IsEquiv.valuedCompletion_le_one_iff`, `Valuation.isEquiv_iff_val_lt_val`, `Valuation.restrict_eq_one_iff`, `Valuation.IsRankOneDiscrete.generator'_lt_one`, `Valuation.isNontrivial_iff_exists_lt_one`, `Valuation.Integers.valuation_irreducible_lt_one`, `Int.padicValuation_eq_one_iff`, `ValuationSubring.mapOfLE_valuation_apply`, `Valuation.Integers.map_le_one`, `Valuation.HasExtension.val_map_eq_iff`, `IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_mem`, `IsDedekindDomain.HeightOneSpectrum.intValuation_singleton`, `Valuation.IsEquiv.restrict`, `Valuation.ext_iff`, `Rat.padicValuation_self`, `Valuation.ltIdeal_v_le_of_mem`, `Valued.isClopen_ball`, `ValuativeRel.ValueGroupWithZero.embed_strictMono`, `Valuation.IsEquiv.pos_iff`, `Valued.exists_coe_eq_v`, `ValuativeRel.ValueGroupWithZero.mk_eq_div`, `Valuation.unit_map_eq`, `Valuation.Integers.le_of_dvd`, `Valuation.hasBasis_nhds_zero`, `Polynomial.valuation_of_mk`, `WeierstrassCurve.hasGoodReduction_iff`, `Valuation.val_lt_one_iff`, `Valuation.IsUniformizer.zpowers_eq_valueGroup`, `ValuativeRel.ValueGroupWithZero.orderMonoidIso_valuation_eq_restrict₀`, `Valuation.val_le_one_or_val_inv_le_one`, `Valuation.map_add_of_distinct_val`, `Valuation.restrict_le_iff`, `Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_strictMono`, `Valuation.map_add`, `Valuation.HasExtension.val_map_lt_iff`, `Valued.is_topological_valuation`, `ArchimedeanClass.FiniteElement.val_add`, `IsValuativeTopology.isOpen_ball`, `Valuation.map_div`, `Valuation.restrict_eq_zero_iff`, `Valuation.one_lt_val_iff`, `WeierstrassCurve.hasMultiplicativeReduction_iff`, `Padic.norm_eq_zpow_log_mulValuation`, `Valuation.restrict_eq_mk`, `ValuativeRel.ValueGroupWithZero.leftInverse_embedding_orderMonoidIso`, `ValuationSubring.valuation_lt_one_or_eq_one`, `PowerSeries.intValuation_eq_of_coe`, `Valuation.one_apply_of_ne_zero`, `Valued.continuous_valuation`, `WithVal.apply_symm_equiv`, `Valuation.val_eq_one_iff`, `Valuation.restrict_lt_iff_lt_embedding`, `LaurentSeries.val_le_one_iff_eq_coe`, `NumberField.HeightOneSpectrum.adicAbv_def`, `AddValuation.toValuation_ofValuation`, `Valued.extension_eq_zero_iff`, `IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def`, `IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer`, `ArchimedeanClass.FiniteElement.not_isUnit_iff_mk_pos`, `WithVal.val_apply_equiv`, `IsValuativeTopology.isClopen_sphere`, `FunctionField.valuedFqtInfty.def`, `Valuation.coe_coe`, `Valuation.subgroups_basis`, `WithVal.apply_equiv`, `Valuation.IsEquiv.one_lt_iff_one_lt`, `Valuation.map_sub_eq_of_lt_right`, `IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd`, `Valuation.map_add_le`, `Valuation.mem_unitGroup_iff`, `Valued.isOpen_sphere`, `Valuation.restrict_le_iff_le_embedding`, `IsDedekindDomain.HeightOneSpectrum.valuation_def`, `ValuationSubring.valuation_le_one`, `NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def`, `Valuation.isEquiv_restrict`, `Valuation.nonempty_rankOne_iff_mulArchimedean`, `LaurentSeries.exists_ratFunc_val_lt`, `ArchimedeanClass.FiniteElement.val_mul`, `Valuation.RankOne.exists_val_lt`, `Valued.hasBasis_nhds_zero`, `Valuation.IsRankOneDiscrete.instIsCyclicSubtypeUnitsMemSubgroupValueGroup`, `IsValuativeTopology.continuous_valuation`, `Padic.mulValuation_toFun`, `IsDedekindDomain.HeightOneSpectrum.valuation_div_le_one_iff`, `IsValuativeTopology.mem_nhds_iff'`, `WeierstrassCurve.HasGoodReduction.goodReduction`, `IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_dvd`, `WithVal.strictMono_valueGroupOrderIso₀`, `Valuation.toMonoidWithZeroHom_one`, `Valuation.map_sub_swap`, `Valuation.isEquiv_iff_val_le_one`, `WithVal.strictMono_valueGroupOrderIso₀_symm`, `Valuation.Integers.not_denselyOrdered_of_isPrincipalIdealRing`, `Valuation.IsUniformizer.val`, `ValuativeRel.exists_valuation_posSubmonoid_div_valuation_posSubmonoid_eq`, `Valuation.HasExtension.val_map_le_one_iff`, `Valuation.map_sub`, `Rat.valuation_le_one_iff_den`, `Valuation.mem_valuationSubring_iff`, `RatFunc.valuation_surjective`, `Valuation.ofAddValuation_apply`, `Valuation.Integers.isIntegral_iff_v_le_one`, `ValuativeExtension.mapValueGroupWithZero_valuation`, `Valuation.isEquiv_iff_val_eq_one`, `WithVal.valueGroupEquiv_apply`, `Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered`, `Polynomial.valuation_inv_monomial_eq_valuation_X_zpow`, `Valuation.RankOne.strictMono`, `Valuation.Integers.le_iff_dvd`, `LaurentSeries.exists_Polynomial_intValuation_lt`, `ValuativeRel.ValueGroupWithZero.embed_valuation_eq_restrict₀`, `ValuationSubring.valuation_le_one_iff`, `Valued.coe_valuation_eq_rankOne_hom_comp_valuation`, `ValuationSubring.mem_unitGroup_iff`, `IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation'`, `Polynomial.valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X`, `ValuativeRel.ValueGroupWithZero.orderMonoidIso_mk`, `ArchimedeanClass.FiniteElement.val_sub`, `Valuation.toAddValuation_apply`, `Valued.isClosed_ball`, `Valuation.zero_iff`, `Valuation.restrict_lt_one_iff`, `Valuation.map_sub_le`, `Valuation.srel_iff_lt`, `Valued.isClopen_sphere`, `PadicAlgCl.valuation_p`, `PadicComplex.valuation_p`, `Valued.isClosed_sphere`, `IsValuativeTopology.isClosed_closedBall`, `FiniteField.valuation_algebraMap_eq_one`, `Polynomial.valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X`, `Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator`, `Valuation.one_apply_eq_zero_iff`, `IsDedekindDomain.HeightOneSpectrum.valuation_of_mk'`, `WithVal.lt_def`, `Valuation.cauchy_iff`, `Valuation.locally_const`, `IsValuativeTopology.mem_nhds_zero_iff`, `ModP.preVal_mk`, `Valuation.apply_posSubmonoid_pos`, `Valuation.one_srel_iff`, `RatFunc.valuation_eq_LaurentSeries_valuation`, `ModP.v_p_lt_preVal`, `Valuation.IsRankOneDiscrete.generator_zpowers_eq_range`, `Valuation.IsRankOneDiscrete.embedding_generator'`, `Valued.locally_const`, `Valuation.mem_leAddSubgroup_iff`, `Valuation.vle_iff_le`, `ValuativeRel.ValueGroupWithZero.orderMonoidIso_embed`, `Valued.toNormedField.norm_le_iff`, `Valuation.map_add'`, `IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_mem`, `Valuation.restrict_inj`, `Valuation.map_sum_lt`, `Valuation.map_add_lt`, `Valued.integer.mulArchimedean_mrange_of_isCompact_integer`, `Valuation.Integers.dvdNotUnit_iff_lt`, `Padic.valuation_p_lt_one`, `LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero`, `Valuation.embedding_restrict`, `Valuation.Integers.valuation_unit`, `Valuation.IsEquiv.lt_iff_lt`, `Valuation.map_mul`, `Valuation.ofAddValuation_toAddValuation`, `Valuation.map_sum_lt'`, `Valued.closure_coe_completion_v_lt`, `Valued.valuation_isClosedMap`, `Int.padicValuation_self`, `Valued.closure_coe_completion_v_mul_v_lt`, `Valued.valuedCompletion_apply`, `Valued.cauchy_iff`, `Valuation.one_apply_le_one`, `Polynomial.valuation_le_one_of_valuation_X_le_one`, `ValuationSubring.valuation_eq_iff`, `ValuativeRel.one_apply_posSubmonoid`, `Valuation.instValuationClass`, `ValuativeRel.trivialRel_eq_ofValuation_one`, `ArchimedeanClass.FiniteResidueField.mk_eq_mk`, `Valuation.comap_apply`, `Valuation.map_add_eq_of_lt_left`, `Valuation.map_one_sub_of_lt`, `IsDedekindDomain.HeightOneSpectrum.adicValued_apply`, `AddValuation.ofValuation_toValuation`, `NumberField.FinitePlace.norm_def_int`, `Valuation.leIdeal_v_le_of_mem`, `Valuation.veq_iff_eq`, `IsValuativeTopology.hasBasis_nhds_zero'`, `Valuation.extendToLocalization_mk'`, `WeierstrassCurve.hasAdditiveReduction_iff`, `Valuation.IsRankOneDiscrete.generator'_zpowers_eq_top`, `Valuation.Integers.maximalIdeal_eq_setOf_le_v_algebraMap`, `WeierstrassCurve.HasAdditiveReduction.additiveReduction`, `Valuation.map_one`, `Valuation.restrict_pos_iff`, `Valuation.one_vlt_iff`, `IsValuativeTopology.isClopen_ball`, `IsValuativeTopology.hasBasis_nhds`, `Valuation.toAddValuation_symm_eq`, `IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd`, `ArchimedeanClass.FiniteElement.val_zero`, `Valuation.one_vle_iff`, `Valuation.restrict_def`, `ArchimedeanClass.FiniteElement.isUnit_iff_mk_eq_zero`, `Valued.toNormedField.one_lt_norm_iff`, `IsDedekindDomain.HeightOneSpectrum.intValuation_zero_lt`, `IsValuativeTopology.hasBasis_nhds_zero`, `Valuation.IsEquiv.eq_zero`, `IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation`, `Valuation.IsNontrivial_iff_exists_one_lt`, `Valuation.IsEquiv.orderMonoidIso_trans`, `WithVal.strictMono_valueGroupEquiv_symm`, `Valuation.mem_ltAddSubgroup_iff`, `Valuation.IsRankOneDiscrete.generator_zpowers_eq_valueGroup`, `LaurentSeries.valuation_LaurentSeries_equal_extension`, `Valuation.isClosed_closedBall`, `Valuation.not_isNontrivial_one`, `RatFunc.v_def`, `ArchimedeanClass.FiniteResidueField.mk_ne_zero`, `Rat.padicValuation_eq_zero_iff`, `Valuation.map_inv`, `IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff`, `Valuation.Integers.wfDvdMonoid_iff_wellFounded_gt_on_v`, `Set.unit_valuation_eq_one`, `IsValuativeTopology.isOpen_closedBall`, `Valuation.integer.v_irreducible_pos`, `FunctionField.inftyValuation.X_zpow`, `Valuation.toTopologicalSpace_eq`, `Valuation.map_sub_eq_of_lt_left`, `ValuativeRel.exists_valuation_div_valuation_eq`, `Valuation.map_apply`, `ArchimedeanClass.FiniteElement.val_one`, `Valuation.IsNontrivial.exists_one_lt`, `IsDedekindDomain.HeightOneSpectrum.intValuation_def`, `PadicAlgCl.valuation_def`, `FunctionField.inftyValuation.X`, `Polynomial.valuation_monomial_eq_valuation_X_pow`, `Valuation.toMonoidWithZeroHom_coe_eq_coe`, `Valuation.map_sum_eq_of_lt`, `Valuation.srel_one_iff`, `RatFunc.setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty`, `PadicAlgCl.valuation_coe`, `Valuation.IsUniformizer.val_pos`, `Valuation.isClopen_ball`, `FunctionField.inftyValuedFqt.def`, `Valuation.vle_one_iff`, `Valuation.IsEquiv.val_sub_one_lt_one_iff`, `Valuation.Integers.coe_span_singleton_eq_setOf_le_v_algebraMap`, `Valuation.IsEquiv.eq_iff`, `IsValuativeTopology.hasBasis_nhds'`, `Valuation.Integers.valuation_pos_iff_ne_zero`, `Valued.isOpen_closedBall`, `Valuation.instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial`, `Valuation.hasBasis_nhds`, `RatFunc.valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X`, `Valuation.IsEquiv.one_le_iff_one_le`, `Valuation.ltSubmodule_v_le_of_mem`, `IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective`, `Valued.mem_nhds_zero`, `Valuation.RankLeOne.exists_val_lt`, `Valuation.HasExtension.val_map_eq_one_iff`, `Valued.isOpen_ball`, `ValuationSubring.mem_principalUnitGroup_iff`, `NormedField.v_eq_valuation`, `Valued.mem_nhds`, `IsDedekindDomain.HeightOneSpectrum.valuationOfNeZero_eq`, `Valuation.IsEquiv.le_iff_le`, `Valuation.map_neg`, `Polynomial.valuation_aeval_monomial_eq_valuation_pow`, `Valuation.isOpen_ball`, `IsNonarchimedeanLocalField.isCompact_closedBall`, `Valued.integer.locallyFiniteOrder_units_mrange_of_isCompact_integer`, `Valued.extensionValuation_apply_coe`, `ValuativeRel.valuation_surjective`, `IsDedekindDomain.HeightOneSpectrum.valuation_surjective`, `Valuation.rel_one_iff`, `Valuation.IsEquiv.eq_one_iff_eq_one`, `LaurentSeries.valuation_surjective`, `LaurentSeries.valuation_coe_ratFunc`, `ValuativeRel.ValueGroupWithZero.embed_mk`, `AddValuation.toValuation_apply`, `Valuation.Integers.isPrincipal_iff_exists_eq_setOf_valuation_le`, `IsValuativeTopology.isClosed_ball`, `Valuation.Integer.not_isUnit_iff_valuation_lt_one`, `PadicComplex.RankOne.hom_eq_embedding`, `WithVal.valueGroupOrderIso₀_symm_restrict`, `Valuation.vlt_one_iff`, `Valuation.map_eq_one_of_forall_lt`, `LaurentSeries.valuation_compare`, `Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_symm_apply`, `ValuativeRel.ValueGroupWithZero.embedding_orderMonoidIso_valuation_eq`, `Valuation.map_add_of_left_eq_zero`, `Valuation.hasBasis_uniformity`, `Valued.toNormedField.norm_def`, `LaurentSeries.tendsto_valuation`, `Valuation.toUniformSpace_eq`, `Valuation.isOpen_sphere`, `Valuation.IsEquiv.le_one_iff_le_one`, `Valuation.integer.coe_span_singleton_eq_setOf_le_v_coe`, `Valuation.norm_def`, `Valuation.Integers.wellFounded_gt_on_v_iff_discrete_mrange`, `Valuation.map_sub_of_right_eq_zero`, `PowerSeries.intValuation_X`, `IsDedekindDomain.HeightOneSpectrum.adicValued_apply'`, `Valuation.exists_div_eq_of_unit`, `Valuation.restrict_le_one_iff`, `Valuation.isClosed_ball`, `Valuation.map_eq_of_sub_lt`, `Valuation.IsEquiv.val_eq`, `Valuation.IsEquiv.orderMonoidIso_eq_refl`, `Valuation.HasExtension.mk_smul_mk`, `ValuationSubring.mem_nonunits_iff`, `Valued.toNormedField.norm_lt_iff`, `Valuation.map_pow`, `Valuation.rel_iff_le`, `Valuation.RankOne.zero_of_hom_zero`, `IsDedekindDomain.HeightOneSpectrum.adicCompletion_valueGroup_eq`, `Valuation.IsEquiv.valueGroup₀Fun_zero`, `Valuation.IsEquiv.valueGroup₀Fun_spec`, `Valuation.Integers.valuation_irreducible_pos`, `NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def`, `Valuation.vlt_iff_lt`, `Valuation.IsUniformizer.iff`, `Valued.hasBasis_uniformity`, `Valuation.mem_ltSubmodule_iff`, `ModP.v_p_lt_val`, `ValuativeRel.valuation_lt_symm_orderMonoidIso`, `Valuation.integer.v_irreducible_lt_one`, `FunctionField.inftyValuation.C`, `Valuation.IsNontrivial.exists_lt_one`, `IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one`, `Valuation.Integers.isUnit_iff_valuation_eq_one`, `FiniteField.valuation_algebraMap_le_one`, `LaurentSeries.valuation_le_iff_coeff_lt_log_eq_zero`, `Valuation.restrict_lt_iff`, `Valuation.extendToLocalization_apply_map_apply`, `Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply`, `Valuation.mem_leIdeal_iff`, `Padic.norm_rat_le_one_iff_padicValuation_le_one`, `Valued.isClosed_closedBall`, `Set.integer_valuation_le_one`, `Valuation.isOpen_closedBall`, `PreTilt.map_eq_zero`, `Valuation.coe_ltAddSubgroup`, `Rat.surjective_padicValuation`, `RatFunc.valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one`, `Valuation.RankOne.isNontrivial_restrict`, `Irreducible.maximalIdeal_pow_eq_setOf_le_v_coe_pow`, `ValuativeRel.ValueGroupWithZero.embedding_embed_valuation_eq`, `AddValuation.toValuation_symm_eq`, `IsDedekindDomain.HeightOneSpectrum.intValuation_exists_uniformizer`, `WithVal.le_def`, `RatFunc.valuation_uniformizingPolynomial_lt_one`, `Valuation.HasExtension.val_map_lt_one_iff`, `ValuativeRel.restrict_lt_orderMonoidIso`, `Valuation.toValuation_ofValuation`, `Valuation.one_le_val_iff`, `IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one`, `ValuationSubring.valuation_eq_one_iff`, `Valuation.Compatible.vle_iff_le`, `Valuation.norm_pos_iff_valuation_pos`, `AddValuation.ofValuation_symm_eq`, `Valuation.map_sub_lt`, `ValuativeRel.ValueGroupWithZero.lift_valuation`, `Valuation.coe_mk`, `Valuation.map_sum_le`, `Valuation.IsEquiv.lt_one_iff_lt_one`, `Valued.continuous_valuation_of_surjective`, `Int.padicValuation_le_one`, `Valuation.isEquiv_iff_val_lt_one`, `WithVal.valuation_equiv_symm`, `NormedField.valuation_apply`, `Valuation.IsUniformizer.val_lt_one`, `NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbv`, `NumberField.FinitePlace.norm_embedding'`, `Valuation.restrict_exists_div_eq`, `WeierstrassCurve.HasMultiplicativeReduction.badReduction`, `Valuation.mem_integer_iff`, `Valuation.one_apply_def`, `Valuation.IsEquiv.orderMonoidIso_spec`, `Valuation.RankOne.hom_eq_zero_iff`, `Valued.isClopen_closedBall`, `Valuation.RankOne.restrict_RankOne_hom_eq`, `WithVal.strictMono_valueGroupEquiv`, `IsValuativeTopology.mem_nhds_iff`, `ValuationSubring.valuation_surjective`, `Valuation.pos_iff`, `Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply_zero`, `Valued.exists_pow_lt_of_le_exp_neg_one`, `IsDedekindDomain.HeightOneSpectrum.valuation_le_one`, `Valuation.map_zero`, `Valuation.RankLeOne.strictMono'`, `Valued.toNormedField.norm_lt_one_iff`, `IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroToFun_eq`, `Valuation.exists_setOf_restrict_le_iff`, `ValuativeRel.ValueGroupWithZero.orderMonoidIso_strictMono`, `Valuation.Integers.one_of_isUnit`, `Valuation.IsRankOneDiscrete.exists_generator_lt_one`, `AddValuation.ofValuation_apply`, `IsValuativeTopology.isOpen_sphere`, `FunctionField.inftyValuation_apply`, `ValuationSubring.mapOfLE_comp_valuation`, `Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply_zpow`, `Valuation.val_le_one_iff`, `NumberField.FinitePlace.norm_embedding_int`, `LaurentSeries.exists_ratFunc_eq_v`, `Valued.toNormedField.one_le_norm_iff`, `Valuation.map_sub_of_left_eq_zero`, `Valuation.ofAddValuation_symm_eq`, `ValuativeRel.ValueGroupWithZero.mk_eq_valuation`, `Valuation.coeff_zero_minpoly`, `Valuation.map_add_supp`, `Valuation.IsRankOneDiscrete.generator_mem_range`, `IsValuativeTopology.isClopen_closedBall`, `Valuation.exists_div_eq_of_surjective`, `Valuation.Integers.maximalIdeal_pow_eq_setOf_le_v_algebraMap_pow`, `IsDedekindDomain.HeightOneSpectrum.intValuation_apply`, `Valuation.mem_nhds_iff`, `Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered_mrange`, `LaurentSeries.valuation_X_pow`, `IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_mem`, `Int.padicValuation_eq_zero_iff`, `Valuation.Integers.dvd_iff_le`, `NumberField.FinitePlace.norm_def`, `ArchimedeanClass.FiniteElement.ext_iff`, `Valuation.is_topological_valuation`, `Valuation.one_rel_iff`, `Valuation.le_one_of_subsingleton`, `Valuation.inversion_estimate`, `Valuation.isClopen_sphere`, `WeierstrassCurve.HasMultiplicativeReduction.multiplicativeReduction`, `Valuation.IsEquiv.orderMonoidIso_symm`, `Valuation.isClosed_sphere`, `Valuation.map_add_of_right_eq_zero`, `Rat.padicValuation_le_one_iff`, `Valuation.one_apply_eq_one_iff`, `IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers`, `Polynomial.valuation_X_eq_neg_one`, `Valued.extensionValuation_toFun`

---

← Back to Index