AdicValuation

📁 Source: Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

Statistics

Metric	Count
Definitions adicAbv, adicAbvDef, adicCompletion, adicCompletionIntegers, adicValued, instAlgebraAdicCompletion, instAlgebraSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, instInhabitedSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, intAdicAbv, intAdicAbvDef, intValuation, intValuationDef, valuation	13
Theorems adicAbv_coe_eq_one_iff, adicAbv_coe_le_one, adicAbv_coe_lt_one_iff, adicAbv_of_algebraMap, adicAbv_of_mk', instIsScalarTower', mul_nonZeroDivisor_mem_adicCompletionIntegers, integers, isUnit_iff_valued_eq_one, mem_units_iff_valued_eq_one, has_uniform_continuous_const_smul', uniformContinuousConstSMul, adicValued_apply, adicValued_apply', algebraMap_adicCompletion, algebraMap_adicCompletionIntegers_apply, coe_algebraMap_mem, coe_mem_adicCompletionIntegers, coe_smul_adicCompletion, coe_smul_adicCompletionIntegers, eq_of_valuation_isEquiv_valuation, instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, instIsNontrivialWithZeroMultiplicativeIntValuation, instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, intAdicAbv_eq_one_iff, intAdicAbv_le_one, intAdicAbv_lt_one_iff, le_max_iff_min_le, map_add_le_max', map_mul', map_one', map_zero', intValuationDef_if_neg, intValuationDef_if_pos, intValuationDef_zero, intValuation_apply, intValuation_def, intValuation_eq_one_iff, intValuation_exists_uniformizer, intValuation_if_neg, intValuation_le_one, intValuation_le_pow_iff_dvd, intValuation_le_pow_iff_mem, intValuation_lt_one_iff_dvd, intValuation_lt_one_iff_mem, intValuation_ne_zero, intValuation_ne_zero', intValuation_singleton, intValuation_zero_lt, isNonarchimedean_adicAbv, isNonarchimedean_adicAbvDef, isNonarchimedean_intAdicAbv, isNonarchimedean_intAdicAbvDef, mem_adicCompletionIntegers, mem_integers_of_valuation_le_one, notMem_adicCompletionIntegers, valuation_def, valuation_div_le_one_iff, valuation_exists_uniformizer, valuation_le_one, valuation_lt_one_iff_dvd, valuation_lt_one_iff_mem, valuation_of_algebraMap, valuation_of_mk', valuation_surjective, valuation_uniformizer_ne_zero, valuedAdicCompletion_def, valuedAdicCompletion_eq_valuation, valuedAdicCompletion_eq_valuation', valuedAdicCompletion_surjective, valuation_le_one_iff_den	71
Total	84

IsDedekindDomain.HeightOneSpectrum

Definitions

Name	Category	Theorems
adicAbv 📖	CompOp	6 math math: isNonarchimedean_adicAbv, adicAbv_coe_le_one, adicAbv_of_algebraMap, adicAbv_coe_eq_one_iff, adicAbv_coe_lt_one_iff, adicAbv_of_mk'
adicAbvDef 📖	CompOp	1 math math: isNonarchimedean_adicAbvDef
adicCompletion 📖	CompOp	46 math math: NumberField.prod_nonarchAbsVal_eq, NumberField.FinitePlace.mk_apply, instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, NumberField.FinitePlace.norm_def', mem_adicCompletionIntegers, NumberField.FinitePlace.embedding_apply, adicCompletion.instIsScalarTower', NumberField.FinitePlace.norm_embedding_eq, LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, equivHeightOneSpectrum_symm_apply, valuedAdicCompletion_def, adicCompletionIntegers.integers, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, NumberField.AdeleRing.algebraMap_snd_apply, algebraMap_adicCompletionIntegers_apply, coe_smul_adicCompletionIntegers, coe_algebraMap_mem, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, NumberField.FinitePlace.norm_lt_one_iff_mem, instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, PadicInt.coe_adicCompletionIntegersEquiv_apply, NumberField.isFinitePlace_iff, NumberField.FinitePlace.coe_apply, NumberField.FinitePlace.norm_def_int, valuedAdicCompletion_eq_valuation, coe_mem_adicCompletionIntegers, IsDedekindDomain.FiniteAdeleRing.ext_iff, LaurentSeries.powerSeries_ext_subring, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, LaurentSeries.powerSeriesRingEquiv_coe_apply, instIsDiscreteValuationRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, valuedAdicCompletion_surjective, NumberField.FinitePlace.norm_eq_one_iff_notMem, LaurentSeries.tendsto_valuation, adicCompletionIntegers.isUnit_iff_valued_eq_one, NumberField.FinitePlace.isFinitePlace, instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, adicCompletionIntegers.mem_units_iff_valued_eq_one, embedding_mul_absNorm, NumberField.FinitePlace.norm_le_one, LaurentSeries.mem_integers_of_powerSeries, algebraMap_adicCompletion, adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers, NumberField.FinitePlace.norm_def, notMem_adicCompletionIntegers
adicCompletionIntegers 📖	CompOp	24 math math: instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, mem_adicCompletionIntegers, adicCompletion.instIsScalarTower', LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, adicCompletionIntegers.integers, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, algebraMap_adicCompletionIntegers_apply, coe_smul_adicCompletionIntegers, coe_algebraMap_mem, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, PadicInt.coe_adicCompletionIntegersEquiv_apply, coe_mem_adicCompletionIntegers, LaurentSeries.powerSeries_ext_subring, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, LaurentSeries.powerSeriesRingEquiv_coe_apply, instIsDiscreteValuationRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, adicCompletionIntegers.isUnit_iff_valued_eq_one, instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, adicCompletionIntegers.mem_units_iff_valued_eq_one, LaurentSeries.mem_integers_of_powerSeries, adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers, notMem_adicCompletionIntegers
adicValued 📖	CompOp	2 math math: adicValued_apply, adicValued_apply'
instAlgebraAdicCompletion 📖	CompOp	9 math math: Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, PadicInt.coe_adicCompletionIntegersEquiv_apply, valuedAdicCompletion_eq_valuation, coe_mem_adicCompletionIntegers, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, algebraMap_adicCompletion, adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers
instAlgebraSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers 📖	CompOp	5 math math: instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, adicCompletion.instIsScalarTower', algebraMap_adicCompletionIntegers_apply, coe_smul_adicCompletionIntegers, instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers
instInhabitedSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers 📖	CompOp	—
intAdicAbv 📖	CompOp	10 math math: intAdicAbv_le_one, Polynomial.contentIdeal_eq_top_iff_forall_gaussNorm_eq_one, Polynomial.gaussNorm_intAdicAbv_le_one, Polynomial.gaussNorm_lt_one_iff_contentIdeal_le, isNonarchimedean_intAdicAbv, intAdicAbv_lt_one_iff, intAdicAbv_eq_one_iff, adicAbv_of_algebraMap, Polynomial.isPrimitive_iff_forall_gaussNorm_eq_one, adicAbv_of_mk'
intAdicAbvDef 📖	CompOp	1 math math: isNonarchimedean_intAdicAbvDef
intValuation 📖	CompOp	20 math math: intValuation_if_neg, valuation_of_algebraMap, intValuation_le_one, intValuation_le_pow_iff_mem, intValuation_singleton, Polynomial.valuation_of_mk, PowerSeries.intValuation_eq_of_coe, intValuation_le_pow_iff_dvd, valuation_def, LaurentSeries.exists_Polynomial_intValuation_lt, valuation_of_mk', NumberField.FinitePlace.norm_def_int, intValuation_lt_one_iff_dvd, intValuation_zero_lt, intValuation_eq_one_iff, intValuation_def, PowerSeries.intValuation_X, intValuation_exists_uniformizer, intValuation_apply, intValuation_lt_one_iff_mem
intValuationDef 📖	CompOp	8 math math: intValuationDef_if_neg, intValuation.map_zero', intValuation.map_add_le_max', intValuation.map_one', intValuationDef_zero, intValuation.map_mul', intValuationDef_if_pos, intValuation_apply
valuation 📖	CompOp	88 math math: adicValued.has_uniform_continuous_const_smul', NumberField.prod_nonarchAbsVal_eq, NumberField.FinitePlace.mk_apply, LaurentSeries.LaurentSeriesRingEquiv_def, instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, Set.unit_eq, NumberField.FinitePlace.norm_def', mem_adicCompletionIntegers, NumberField.FinitePlace.embedding_apply, valuation_of_algebraMap, instIsDiscreteValuationRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation, WeierstrassCurve.valuation_Δ_aux_eq_of_isIntegral, instIsNontrivialWithZeroMultiplicativeIntValuation, adicCompletion.instIsScalarTower', NumberField.FinitePlace.norm_embedding_eq, Polynomial.valuation_of_mk, LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, equivHeightOneSpectrum_symm_apply, valuedAdicCompletion_def, valuation_exists_uniformizer, IsDiscreteValuationRing.isRankOneDiscrete, adicCompletionIntegers.integers, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, NumberField.AdeleRing.algebraMap_snd_apply, algebraMap_adicCompletionIntegers_apply, coe_smul_adicCompletionIntegers, coe_algebraMap_mem, valuation_def, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, valuation_div_le_one_iff, valuation_lt_one_iff_dvd, NumberField.FinitePlace.norm_lt_one_iff_mem, Rat.valuation_le_one_iff_den, WeierstrassCurve.isGoodReduction_iff, valuedAdicCompletion_eq_valuation', instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, valuation_of_mk', RatFunc.valuation_eq_LaurentSeries_valuation, PadicInt.coe_adicCompletionIntegersEquiv_apply, NumberField.isFinitePlace_iff, valuation_lt_one_iff_mem, LaurentSeries.coe_X_compare, NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def, NumberField.FinitePlace.coe_apply, adicValued_apply, NumberField.FinitePlace.norm_def_int, IsDiscreteValuationRing.map_algebraMap_eq_valuationSubring, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, valuedAdicCompletion_eq_valuation, coe_mem_adicCompletionIntegers, RatFunc.v_def, LaurentSeries.powerSeries_ext_subring, Set.unit_valuation_eq_one, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, LaurentSeries.powerSeriesRingEquiv_coe_apply, instIsDiscreteValuationRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, adicValued.uniformContinuousConstSMul, valuedAdicCompletion_surjective, valuationOfNeZero_eq, valuation_surjective, NumberField.FinitePlace.norm_eq_one_iff_notMem, LaurentSeries.valuation_compare, LaurentSeries.tendsto_valuation, adicValued_apply', NumberField.toNNReal_valued_eq_adicAbv, LaurentSeries.valuation_def, adicCompletionIntegers.isUnit_iff_valued_eq_one, Rat.HeightOneSpectrum.valuation_equiv_padicValuation, Set.integer_valuation_le_one, coe_smul_adicCompletion, NumberField.FinitePlace.isFinitePlace, instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, LaurentSeries.ratfuncAdicComplRingEquiv_apply, adicCompletionIntegers.mem_units_iff_valued_eq_one, Set.integer_eq, embedding_mul_absNorm, NumberField.FinitePlace.norm_le_one, LaurentSeries.mem_integers_of_powerSeries, WeierstrassCurve.IsGoodReduction.goodReduction, algebraMap_adicCompletion, adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers, valuation_le_one, instIsPrincipalIdealRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation, valuationOfNeZeroToFun_eq, NumberField.FinitePlace.norm_def, notMem_adicCompletionIntegers, Polynomial.valuation_X_eq_neg_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adicAbv_coe_eq_one_iff 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal	DFunLike.coe AbsoluteValue Real DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Real.semiring Real.partialOrder AbsoluteValue.funLike adicAbv RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap Real.instOne Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule asIdeal	—	adicAbv_of_algebraMap intAdicAbv_eq_one_iff
adicAbv_coe_le_one 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal	Real Real.instLE DFunLike.coe AbsoluteValue DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Real.semiring Real.partialOrder AbsoluteValue.funLike adicAbv RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap Real.instOne	—	adicAbv_of_algebraMap intAdicAbv_le_one
adicAbv_coe_lt_one_iff 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal	Real Real.instLT DFunLike.coe AbsoluteValue DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Real.semiring Real.partialOrder AbsoluteValue.funLike adicAbv RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap Real.instOne Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule asIdeal	—	adicAbv_of_algebraMap intAdicAbv_lt_one_iff
adicAbv_of_algebraMap 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal	DFunLike.coe AbsoluteValue Real DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Real.semiring Real.partialOrder AbsoluteValue.funLike adicAbv RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap intAdicAbv	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing valuation_of_algebraMap
adicAbv_of_mk' 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal	DFunLike.coe AbsoluteValue Real DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Real.semiring Real.partialOrder AbsoluteValue.funLike adicAbv IsLocalization.mk' CommRing.toCommSemiring nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring Semifield.toCommSemiring DivInvMonoid.toDiv Real.instDivInvMonoid intAdicAbv Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsFractionRing.mk'_eq_div map_div₀ AbsoluteValue.monoidWithZeroHomClass Real.instIsDomain IsLocalRing.toNontrivial Field.instIsLocalRing valuation_of_algebraMap
adicValued_apply 📖	mathematical	—	DFunLike.coe Valuation WithZero Multiplicative LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike Valued.v adicValued WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing valuation	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid
adicValued_apply' 📖	mathematical	—	DFunLike.coe Valuation WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid DivisionRing.toRing Field.toDivisionRing valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithVal.instField Valuation.instFunLike Valued.v adicValued WithVal.instAlgebra_2 WithVal.instIsFractionRing EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid WithVal.instIsFractionRing
algebraMap_adicCompletion 📖	mathematical	—	DFunLike.coe RingHom adicCompletion Semiring.toNonAssocSemiring CommSemiring.toSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield UniformSpace.Completion.instField WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing valuation WithVal.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup RingHom.instFunLike algebraMap instAlgebraAdicCompletion UniformSpace.Completion.coe'	—	Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup
algebraMap_adicCompletionIntegers_apply 📖	mathematical	—	adicCompletion ValuationSubring UniformSpace.Completion.instField WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing valuation WithVal.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SetLike.instMembership ValuationSubring.instSetLike adicCompletionIntegers DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass UniformSpace.Completion.ring IsTopologicalDivisionRing.toIsTopologicalRing UniformSpace.toTopologicalSpace ValuationSubring.instSubringClass RingHom.instFunLike algebraMap instAlgebraSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers UniformSpace.Completion.coe' DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SubringClass.toSubsemiringClass IsTopologicalDivisionRing.toIsTopologicalRing ValuationSubring.instSubringClass
coe_algebraMap_mem 📖	mathematical	—	adicCompletion ValuationSubring UniformSpace.Completion.instField WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing valuation WithVal.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SetLike.instMembership ValuationSubring.instSetLike adicCompletionIntegers UniformSpace.Completion.coe' DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap	—	Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup IsTopologicalDivisionRing.toIsTopologicalRing mem_adicCompletionIntegers Valued.valuedCompletion_apply valuation_le_one
coe_mem_adicCompletionIntegers 📖	mathematical	—	adicCompletion ValuationSubring UniformSpace.Completion.instField WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing valuation WithVal.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SetLike.instMembership ValuationSubring.instSetLike adicCompletionIntegers Algebra.cast CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instAlgebraAdicCompletion	—	Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup IsTopologicalDivisionRing.toIsTopologicalRing mem_adicCompletionIntegers Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing valuedAdicCompletion_eq_valuation valuation_le_one
coe_smul_adicCompletion 📖	mathematical	—	UniformSpace.Completion.coe' WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid DivisionRing.toRing Field.toDivisionRing valuation Valued.toUniformSpace WithVal.instRing WithVal.instValued WithVal.instSMul Algebra.toSMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield UniformSpace.Completion UniformSpace.Completion.instSMul	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid UniformSpace.Completion.coe_smul adicValued.uniformContinuousConstSMul
coe_smul_adicCompletionIntegers 📖	mathematical	—	adicCompletion ValuationSubring UniformSpace.Completion.instField WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing valuation WithVal.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SetLike.instMembership ValuationSubring.instSetLike adicCompletionIntegers Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass UniformSpace.Completion.ring IsTopologicalDivisionRing.toIsTopologicalRing UniformSpace.toTopologicalSpace ValuationSubring.instSubringClass instAlgebraSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers UniformSpace.Completion.instSMul WithVal.instSMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SubringClass.toSubsemiringClass IsTopologicalDivisionRing.toIsTopologicalRing ValuationSubring.instSubringClass
eq_of_valuation_isEquiv_valuation 📖	—	Valuation.IsEquiv WithZero Multiplicative DivisionRing.toRing Field.toDivisionRing WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing valuation	—	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid valuation_lt_one_iff_mem
instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers 📖	mathematical	—	FaithfulSMul adicCompletion ValuationSubring UniformSpace.Completion.instField WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing valuation WithVal.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SetLike.instMembership ValuationSubring.instSetLike adicCompletionIntegers Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass UniformSpace.Completion.ring IsTopologicalDivisionRing.toIsTopologicalRing UniformSpace.toTopologicalSpace ValuationSubring.instSubringClass instAlgebraSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers	—	Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SubringClass.toSubsemiringClass IsTopologicalDivisionRing.toIsTopologicalRing ValuationSubring.instSubringClass faithfulSMul_iff_algebraMap_injective CompletableTopField.toT0Space FaithfulSMul.algebraMap_injective
instIsNontrivialWithZeroMultiplicativeIntValuation 📖	mathematical	—	Valuation.IsNontrivial WithZero Multiplicative DivisionRing.toRing Field.toDivisionRing WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing valuation	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing valuation_exists_uniformizer
instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers 📖	mathematical	—	Module.IsTorsionFree adicCompletion ValuationSubring UniformSpace.Completion.instField WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing valuation WithVal.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SetLike.instMembership ValuationSubring.instSetLike adicCompletionIntegers CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ValuationSubring.instCommRingSubtypeMem Algebra.toModule SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass UniformSpace.Completion.ring IsTopologicalDivisionRing.toIsTopologicalRing UniformSpace.toTopologicalSpace ValuationSubring.instSubringClass instAlgebraSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers	—	Module.IsTorsionFree.of_smul_eq_zero Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SubringClass.toSubsemiringClass IsTopologicalDivisionRing.toIsTopologicalRing ValuationSubring.instSubringClass IsDomain.toNontrivial IsDedekindDomain.toIsDomain FaithfulSMul.to_isTorsionFree instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers IsFractionRing.instFaithfulSMul IsDomain.toIsCancelMulZero ValuationSubring.instIsDomainSubtypeMem
intAdicAbv_eq_one_iff 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal	DFunLike.coe AbsoluteValue Real CommSemiring.toSemiring CommRing.toCommSemiring Real.semiring Real.partialOrder AbsoluteValue.funLike intAdicAbv Real.instOne Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule asIdeal	—	Mathlib.Tactic.Contrapose.contrapose_iff₃ intAdicAbv_lt_one_iff ne_iff_lt_iff_le intAdicAbv_le_one
intAdicAbv_le_one 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal	Real Real.instLE DFunLike.coe AbsoluteValue CommSemiring.toSemiring CommRing.toCommSemiring Real.semiring Real.partialOrder AbsoluteValue.funLike intAdicAbv Real.instOne	—	ne_zero_of_lt WithZeroMulInt.toNNReal_le_one_iff intValuation_le_one
intAdicAbv_lt_one_iff 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal	Real Real.instLT DFunLike.coe AbsoluteValue CommSemiring.toSemiring CommRing.toCommSemiring Real.semiring Real.partialOrder AbsoluteValue.funLike intAdicAbv Real.instOne Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule asIdeal	—	ne_zero_of_lt WithZeroMulInt.toNNReal_lt_one_iff intValuation_lt_one_iff_mem
intValuationDef_if_neg 📖	mathematical	—	intValuationDef WithZero.exp Associates.count Ideal CommSemiring.toSemiring CommRing.toCommSemiring CommSemiring.toCommMonoidWithZero IdemCommSemiring.toCommSemiring Ideal.instIdemCommSemiring Associated.setoid MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero Irreducible Associates Associates.instCommMonoidWithZero Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id asIdeal Associates.factors Ideal.uniqueFactorizationMonoid Ideal.span Set Set.instSingletonSet	—	Ideal.uniqueFactorizationMonoid
intValuationDef_if_pos 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	intValuationDef WithZero Multiplicative WithZero.instZero	—	Ideal.uniqueFactorizationMonoid
intValuationDef_zero 📖	mathematical	—	intValuationDef MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing WithZero Multiplicative WithZero.instZero	—	Ideal.uniqueFactorizationMonoid
intValuation_apply 📖	mathematical	—	DFunLike.coe Valuation WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing Valuation.instFunLike intValuation intValuationDef	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing
intValuation_def 📖	mathematical	—	DFunLike.coe Valuation WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing Valuation.instFunLike intValuation MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing WithZero.instZero WithZero.exp Associates.count Ideal CommSemiring.toSemiring CommRing.toCommSemiring CommSemiring.toCommMonoidWithZero IdemCommSemiring.toCommSemiring Ideal.instIdemCommSemiring Associated.setoid MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero Irreducible Associates Associates.instCommMonoidWithZero Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id asIdeal Associates.factors Ideal.uniqueFactorizationMonoid Ideal.span Set Set.instSingletonSet	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing
intValuation_eq_one_iff 📖	mathematical	—	DFunLike.coe Valuation WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing Valuation.instFunLike intValuation WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule asIdeal	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Iff.not intValuation_lt_one_iff_mem le_antisymm intValuation_le_one
intValuation_exists_uniformizer 📖	mathematical	—	DFunLike.coe Valuation WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing Valuation.instFunLike intValuation WithZero.exp	—	associates_irreducible Ideal.dvdNotUnit_iff_lt ne_bot Iff.not Ideal.isUnit_iff Ideal.IsPrime.ne_top isPrime sq Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing SetLike.exists_of_lt instIsConcreteLE Associates.mk_ne_zero' Submodule.zero_mem Ideal.uniqueFactorizationMonoid intValuation_if_neg Associates.prime_pow_dvd_iff_le pow_one Associates.mk_le_mk_iff_dvd IsScalarTower.right Ideal.dvd_span_singleton not_le Associates.mk_pow
intValuation_if_neg 📖	mathematical	—	DFunLike.coe Valuation WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing Valuation.instFunLike intValuation WithZero.exp Associates.count Ideal CommSemiring.toSemiring CommRing.toCommSemiring CommSemiring.toCommMonoidWithZero IdemCommSemiring.toCommSemiring Ideal.instIdemCommSemiring Associated.setoid MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero Irreducible Associates Associates.instCommMonoidWithZero Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id asIdeal Associates.factors Ideal.uniqueFactorizationMonoid Ideal.span Set Set.instSingletonSet	—	intValuationDef_if_neg
intValuation_le_one 📖	mathematical	—	WithZero Multiplicative Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe Valuation WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing Valuation.instFunLike intValuation WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Valuation.map_zero WithZero.zero_le Ideal.uniqueFactorizationMonoid intValuation_if_neg WithZero.exp_zero WithZero.exp_le_exp Right.neg_nonpos_iff covariant_swap_add_of_covariant_add Int.instAddLeftMono
intValuation_le_pow_iff_dvd 📖	mathematical	—	WithZero Multiplicative Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe Valuation WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing Valuation.instFunLike intValuation WithZero.exp Ideal CommSemiring.toSemiring CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Submodule.instNonUnitalSemiring Semiring.toModule IsScalarTower.right Algebra.id Submodule.instPowNat asIdeal Ideal.span Set Set.instSingletonSet	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsScalarTower.right Valuation.map_zero Ideal.uniqueFactorizationMonoid intValuation_if_neg WithZero.exp_le_exp neg_le_neg_iff Int.instAddLeftMono covariant_swap_add_of_covariant_add Ideal.dvd_span_singleton Associates.le_singleton_iff Associates.prime_pow_dvd_iff_le Associates.mk_ne_zero' associates_irreducible
intValuation_le_pow_iff_mem 📖	mathematical	—	WithZero Multiplicative Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe Valuation WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing Valuation.instFunLike intValuation WithZero.exp Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id asIdeal	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsScalarTower.right intValuation_le_pow_iff_dvd Ideal.dvd_span_singleton
intValuation_lt_one_iff_dvd 📖	mathematical	—	WithZero Multiplicative Preorder.toLT WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe Valuation WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing Valuation.instFunLike intValuation WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing Ideal CommSemiring.toSemiring CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Submodule.instNonUnitalSemiring Semiring.toModule IsScalarTower.right Algebra.id asIdeal Ideal.span Set Set.instSingletonSet	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsScalarTower.right map_zero MonoidWithZeroHomClass.toZeroHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass LinearOrderedCommMonoidWithZero.toZeroLeOneClass NeZero.one WithZero.instNontrivial Ideal.span_singleton_zero Ideal.uniqueFactorizationMonoid intValuation_if_neg WithZero.exp_zero WithZero.exp_lt_exp neg_lt_zero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Int.instAddLeftMono zero_lt_iff Ideal.zero_eq_bot Ideal.span_singleton_eq_bot Associates.count_ne_zero_iff_dvd irreducible
intValuation_lt_one_iff_mem 📖	mathematical	—	WithZero Multiplicative Preorder.toLT WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe Valuation WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing Valuation.instFunLike intValuation WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule asIdeal	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsScalarTower.right intValuation_lt_one_iff_dvd Ideal.dvd_span_singleton
intValuation_ne_zero 📖	—	—	—	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Ideal.uniqueFactorizationMonoid intValuation_if_neg WithZero.coe_ne_zero
intValuation_ne_zero' 📖	—	—	—	—	intValuation_ne_zero nonZeroDivisors.coe_ne_zero IsDomain.toNontrivial IsDedekindDomain.toIsDomain
intValuation_singleton 📖	mathematical	asIdeal Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instSingletonSet	DFunLike.coe Valuation WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing Valuation.instFunLike intValuation WithZero.exp	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Ideal.uniqueFactorizationMonoid intValuation_if_neg Associates.count_self Ideal.instNontrivial IsDomain.toNontrivial IsDedekindDomain.toIsDomain associates_irreducible
intValuation_zero_lt 📖	mathematical	—	WithZero Multiplicative Preorder.toLT WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt WithZero.instZero DFunLike.coe Valuation WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing Valuation.instFunLike intValuation Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisors	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Ideal.uniqueFactorizationMonoid intValuation_if_neg nonZeroDivisors.coe_ne_zero IsDomain.toNontrivial IsDedekindDomain.toIsDomain WithZero.zero_lt_coe
isNonarchimedean_adicAbv 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal	IsNonarchimedean Real Real.linearOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain DFunLike.coe AbsoluteValue DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Real.semiring Real.partialOrder AbsoluteValue.funLike adicAbv	—	isNonarchimedean_adicAbvDef
isNonarchimedean_adicAbvDef 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal	IsNonarchimedean NNReal.instLinearOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain adicAbvDef	—	ne_zero_of_lt StrictMono.monotone WithZeroMulInt.toNNReal_strictMono Monotone.map_max Valuation.map_add Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing
isNonarchimedean_intAdicAbv 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal	IsNonarchimedean Real Real.linearOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe AbsoluteValue CommSemiring.toSemiring CommRing.toCommSemiring Real.semiring Real.partialOrder AbsoluteValue.funLike intAdicAbv	—	isNonarchimedean_intAdicAbvDef
isNonarchimedean_intAdicAbvDef 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal	IsNonarchimedean NNReal.instLinearOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing intAdicAbvDef	—	ne_zero_of_lt StrictMono.monotone WithZeroMulInt.toNNReal_strictMono Monotone.map_max Valuation.map_add Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing
mem_adicCompletionIntegers 📖	mathematical	—	adicCompletion ValuationSubring UniformSpace.Completion.instField WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing valuation WithVal.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SetLike.instMembership ValuationSubring.instSetLike adicCompletionIntegers Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero UniformSpace.Completion.ring IsTopologicalDivisionRing.toIsTopologicalRing UniformSpace.toTopologicalSpace Valuation.instFunLike Valued.v Valued.valuedCompletion WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup
mem_integers_of_valuation_le_one 📖	mathematical	WithZero Multiplicative Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe Valuation WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike valuation WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	Subring SetLike.instMembership Subring.instSetLike RingHom.range CommRing.toRing algebraMap CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsLocalization.surj eq_or_ne IsFractionRing.mk'_eq_div map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass zero_div AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass SubringClass.toSubsemiringClass Subring.instSubringClass nonZeroDivisors.ne_zero IsDomain.toNontrivial IsDedekindDomain.toIsDomain IsScalarTower.right Ideal.span_singleton_eq_bot Associates.mk_le_mk_iff_dvd Ideal.uniqueFactorizationMonoid Associates.factors_le WithTop.coe_le_coe Multiset.le_iff_count Associates.mk_surjective sub_neg_eq_add Int.instAddLeftMono add_zero Int.instZeroLEOneClass Int.instCharZero Associates.count_some Associates.count.congr_simp Ideal.isPrime_of_prime irreducible_iff_prime Ideal.isCancelMulZero UniqueFactorizationMonoid.instDecompositionMonoid Prime.ne_zero intValuation_if_neg valuation_of_mk' Ideal.span_singleton_le_span_singleton Ideal.le_of_dvd mul_eq_mul_left_iff IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero instIsDomain mul_comm map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Module.IsTorsionFree.to_faithfulSMul IsLocalRing.toNontrivial Field.instIsLocalRing FaithfulSMul.to_isTorsionFree IsFractionRing.instFaithfulSMul IsLocalization.eq_mk'_iff_mul_eq
notMem_adicCompletionIntegers 📖	mathematical	—	adicCompletion ValuationSubring UniformSpace.Completion.instField WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing valuation WithVal.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SetLike.instMembership ValuationSubring.instSetLike adicCompletionIntegers Preorder.toLT WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero UniformSpace.Completion.ring IsTopologicalDivisionRing.toIsTopologicalRing UniformSpace.toTopologicalSpace Valuation.instFunLike Valued.v Valued.valuedCompletion	—	Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup IsTopologicalDivisionRing.toIsTopologicalRing mem_adicCompletionIntegers not_le
valuation_def 📖	mathematical	—	DFunLike.coe Valuation WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid CommRing.toRing EuclideanDomain.toCommRing Field.toEuclideanDomain Valuation.extendToLocalization intValuation nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Set.mem_compl SetLike.coe Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Valuation.supp intValuation_ne_zero' Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing
valuation_div_le_one_iff 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule asIdeal	WithZero Multiplicative Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe Valuation WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike valuation DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Algebra.cast DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Mathlib.Tactic.Contrapose.contrapose₃ AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass Valuation.ne_zero_iff WithZero.instNontrivial IsFractionRing.instFaithfulSMul WithZero.log_lt_log one_ne_zero NeZero.one map_div₀ ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass WithZero.log_div WithZero.log_one valuation_of_algebraMap intValuation_eq_one_iff div_one
valuation_exists_uniformizer 📖	mathematical	—	DFunLike.coe Valuation WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike valuation WithZero.exp	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing intValuation_exists_uniformizer Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid Set.mem_compl intValuation_ne_zero' valuation_def Valuation.extendToLocalization_apply_map_apply
valuation_le_one 📖	mathematical	—	WithZero Multiplicative Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe Valuation WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike valuation Algebra.cast CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing valuation_of_algebraMap intValuation_le_one
valuation_lt_one_iff_dvd 📖	mathematical	—	WithZero Multiplicative Preorder.toLT WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe Valuation WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike valuation Algebra.cast CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing Ideal CommSemiring.toSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Submodule.instNonUnitalSemiring Semiring.toModule IsScalarTower.right Algebra.id asIdeal Ideal.span Set Set.instSingletonSet	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsScalarTower.right valuation_of_algebraMap intValuation_lt_one_iff_dvd
valuation_lt_one_iff_mem 📖	mathematical	—	WithZero Multiplicative Preorder.toLT WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe Valuation WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike valuation Algebra.cast CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule asIdeal	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing valuation_of_algebraMap intValuation_lt_one_iff_mem
valuation_of_algebraMap 📖	mathematical	—	DFunLike.coe Valuation WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike valuation Algebra.cast CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield CommRing.toRing intValuation	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid Set.mem_compl intValuation_ne_zero' valuation_def Valuation.extendToLocalization_apply_map_apply
valuation_of_mk' 📖	mathematical	—	DFunLike.coe Valuation WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike valuation IsLocalization.mk' CommRing.toCommSemiring nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield WithZero.div Multiplicative.div CommRing.toRing intValuation Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid Set.mem_compl intValuation_ne_zero' valuation_def Valuation.extendToLocalization_mk' div_eq_mul_inv
valuation_surjective 📖	mathematical	—	WithZero Multiplicative DFunLike.coe Valuation WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike valuation	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing GroupWithZero.eq_zero_or_unit WithZero.instNontrivial ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass valuation_exists_uniformizer zpow_neg map_inv₀ map_zpow₀ inv_zpow' mul_one WithZero.exp_log inv_inv
valuation_uniformizer_ne_zero 📖	—	—	—	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing valuation_exists_uniformizer Valuation.ne_zero_iff WithZero.instNontrivial ne_of_eq_of_ne WithZero.coe_ne_zero
valuedAdicCompletion_def 📖	mathematical	—	DFunLike.coe Valuation adicCompletion WithZero Multiplicative LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder UniformSpace.Completion.ring WithVal DivisionRing.toRing Field.toDivisionRing valuation Valued.toUniformSpace WithVal.instValued IsTopologicalDivisionRing.toIsTopologicalRing UniformSpace.toTopologicalSpace Valued.isTopologicalDivisionRing Valued.toIsUniformAddGroup Valuation.instFunLike Valued.v Valued.valuedCompletion Valued.extension	—	IsTopologicalDivisionRing.toIsTopologicalRing Valued.isTopologicalDivisionRing Valued.toIsUniformAddGroup
valuedAdicCompletion_eq_valuation 📖	mathematical	—	DFunLike.coe Valuation adicCompletion WithZero Multiplicative LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder UniformSpace.Completion.ring WithVal DivisionRing.toRing Field.toDivisionRing valuation Valued.toUniformSpace WithVal.instValued IsTopologicalDivisionRing.toIsTopologicalRing UniformSpace.toTopologicalSpace Valued.isTopologicalDivisionRing Valued.toIsUniformAddGroup Valuation.instFunLike Valued.v Valued.valuedCompletion Algebra.cast CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield UniformSpace.Completion.instField WithVal.instField WithVal.instRing Valued.completable instAlgebraAdicCompletion WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing	—	IsTopologicalDivisionRing.toIsTopologicalRing Valued.isTopologicalDivisionRing Valued.toIsUniformAddGroup Valued.completable Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid Valued.valuedCompletion_apply
valuedAdicCompletion_eq_valuation' 📖	mathematical	—	DFunLike.coe Valuation UniformSpace.Completion WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing valuation Valued.toUniformSpace WithVal.instRing WithVal.instValued LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero UniformSpace.Completion.ring IsTopologicalDivisionRing.toIsTopologicalRing UniformSpace.toTopologicalSpace Valued.isTopologicalDivisionRing Valued.toIsUniformAddGroup Valuation.instFunLike Valued.v Valued.valuedCompletion UniformSpace.Completion.coe' WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing	—	IsTopologicalDivisionRing.toIsTopologicalRing Valued.isTopologicalDivisionRing Valued.toIsUniformAddGroup Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid Valued.valuedCompletion_apply
valuedAdicCompletion_surjective 📖	mathematical	—	adicCompletion WithZero Multiplicative DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder UniformSpace.Completion.ring WithVal DivisionRing.toRing Field.toDivisionRing valuation Valued.toUniformSpace WithVal.instValued IsTopologicalDivisionRing.toIsTopologicalRing UniformSpace.toTopologicalSpace Valued.isTopologicalDivisionRing Valued.toIsUniformAddGroup Valuation.instFunLike Valued.v Valued.valuedCompletion	—	IsTopologicalDivisionRing.toIsTopologicalRing Valued.isTopologicalDivisionRing Valued.toIsUniformAddGroup Valued.valuedCompletion_surjective_iff valuation_surjective

IsDedekindDomain.HeightOneSpectrum.adicCompletion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsScalarTower' 📖	mathematical	—	IsScalarTower IsDedekindDomain.HeightOneSpectrum.adicCompletion ValuationSubring UniformSpace.Completion.instField WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing IsDedekindDomain.HeightOneSpectrum.valuation WithVal.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SetLike.instMembership ValuationSubring.instSetLike IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass UniformSpace.Completion.ring IsTopologicalDivisionRing.toIsTopologicalRing UniformSpace.toTopologicalSpace ValuationSubring.instSubringClass IsDedekindDomain.HeightOneSpectrum.instAlgebraSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers DivisionSemiring.toSemiring Semifield.toDivisionSemiring ValuationSubring.instAlgebraSubtypeMem UniformSpace.Completion.instSMul WithVal.instSMul	—	Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SubringClass.toSubsemiringClass IsTopologicalDivisionRing.toIsTopologicalRing ValuationSubring.instSubringClass Algebra.smul_def mul_assoc
mul_nonZeroDivisor_mem_adicCompletionIntegers 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisors IsDedekindDomain.HeightOneSpectrum.adicCompletion ValuationSubring UniformSpace.Completion.instField WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing IsDedekindDomain.HeightOneSpectrum.valuation WithVal.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup ValuationSubring.instSetLike IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers UniformSpace.Completion.mul Algebra.cast DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield IsDedekindDomain.HeightOneSpectrum.instAlgebraAdicCompletion	—	Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mul_one Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsDedekindDomain.HeightOneSpectrum.intValuation_exists_uniformizer IsTopologicalDivisionRing.toIsTopologicalRing IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap map_zero MonoidWithZeroHomClass.toZeroHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass WithZero.exp_ne_zero pow_mem mem_nonZeroDivisors_of_ne_zero IsDomain.to_noZeroDivisors IsDedekindDomain.toIsDomain map_pow map_mul MonoidHomClass.toMulHomClass inv_pow nsmul_one Int.natCast_natAbs mul_inv_le_one_of_le₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE LinearOrderedCommMonoidWithZero.toMulPosStrictMono LinearOrderedCommMonoidWithZero.toZeroLeOneClass LE.le.trans WithZero.le_exp_log WithZero.zero_le

IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integers 📖	mathematical	—	Valuation.Integers IsDedekindDomain.HeightOneSpectrum.adicCompletion WithZero Multiplicative UniformSpace.Completion.commRing WithVal WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing IsDedekindDomain.HeightOneSpectrum.valuation WithVal.instCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.toIsUniformAddGroup IsTopologicalDivisionRing.toIsTopologicalRing WithVal.instField UniformSpace.toTopologicalSpace Valued.isTopologicalDivisionRing Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid Valued.v UniformSpace.Completion.ring Valued.valuedCompletion ValuationSubring UniformSpace.Completion.instField Valued.completable SetLike.instMembership ValuationSubring.instSetLike IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ValuationSubring.instCommRingSubtypeMem ValuationSubring.instAlgebraSubtypeMem	—	Valued.toIsUniformAddGroup IsTopologicalDivisionRing.toIsTopologicalRing Valued.isTopologicalDivisionRing Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid Valued.completable FaithfulSMul.algebraMap_injective Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero SubringClass.toSubsemiringClass ValuationSubring.instSubringClass ValuationSubring.instIsDomainSubtypeMem IsLocalRing.toNontrivial Field.instIsLocalRing FaithfulSMul.to_isTorsionFree Subsemiring.instFaithfulSMulSubtypeMem Module.Free.instFaithfulSMulOfNontrivial Module.free_of_finite_type_torsion_free' EuclideanDomain.to_principal_ideal_domain instIsDomain Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors SubsemiringClass.nontrivial
isUnit_iff_valued_eq_one 📖	mathematical	—	IsUnit IsDedekindDomain.HeightOneSpectrum.adicCompletion ValuationSubring UniformSpace.Completion.instField WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing IsDedekindDomain.HeightOneSpectrum.valuation WithVal.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SetLike.instMembership ValuationSubring.instSetLike IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass UniformSpace.Completion.ring IsTopologicalDivisionRing.toIsTopologicalRing UniformSpace.toTopologicalSpace ValuationSubring.instSubringClass DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike Valued.v Valued.valuedCompletion WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SubringClass.toSubsemiringClass IsTopologicalDivisionRing.toIsTopologicalRing ValuationSubring.instSubringClass Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid Valuation.Integers.isUnit_iff_valuation_eq_one integers
mem_units_iff_valued_eq_one 📖	mathematical	—	Units IsDedekindDomain.HeightOneSpectrum.adicCompletion MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield UniformSpace.Completion.instField WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing IsDedekindDomain.HeightOneSpectrum.valuation WithVal.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike Submonoid.units Subsemiring.toSubmonoid Semiring.toNonAssocSemiring Ring.toSemiring Subring.toSubsemiring ValuationSubring.toSubring IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero UniformSpace.Completion.ring IsTopologicalDivisionRing.toIsTopologicalRing UniformSpace.toTopologicalSpace Valuation.instFunLike Valued.v Valued.valuedCompletion Units.val WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup IsTopologicalDivisionRing.toIsTopologicalRing SubringClass.toSubsemiringClass ValuationSubring.instSubringClass isUnit_iff_valued_eq_one Eq.le Units.val_inv_eq_inv_val map_inv₀ ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass LinearOrderedCommMonoidWithZero.toPosMulStrictMono Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing LinearOrderedCommMonoidWithZero.toZeroLeOneClass WithZero.instNontrivial IsLocalRing.toNontrivial Field.instIsLocalRing

IsDedekindDomain.HeightOneSpectrum.adicValued

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
has_uniform_continuous_const_smul' 📖	mathematical	—	UniformContinuousConstSMul WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid DivisionRing.toRing Field.toDivisionRing IsDedekindDomain.HeightOneSpectrum.valuation Valued.toUniformSpace WithVal.instRing WithVal.instValued WithVal.instSMul Algebra.toSMul CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	uniformContinuousConstSMul_of_continuousConstSMul Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid Valued.toIsUniformAddGroup SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing Valued.isTopologicalDivisionRing
uniformContinuousConstSMul 📖	mathematical	—	UniformContinuousConstSMul WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid DivisionRing.toRing Field.toDivisionRing IsDedekindDomain.HeightOneSpectrum.valuation Valued.toUniformSpace WithVal.instRing WithVal.instValued WithVal.instSMul Algebra.toSMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid Algebra.smul_def UniformContinuousConstSMul.uniformContinuous_const_smul Ring.uniformContinuousConstSMul Valued.toIsUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing Valued.isTopologicalDivisionRing

IsDedekindDomain.HeightOneSpectrum.intValuation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_max_iff_min_le 📖	mathematical	—	Multiplicative instLEMultiplicative DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Multiplicative.linearOrder Int.instLinearOrder	—	le_max_iff Multiplicative.ofAdd_le neg_le_neg_iff Int.instAddLeftMono covariant_swap_add_of_covariant_add min_le_iff
map_add_le_max' 📖	mathematical	—	WithZero Multiplicative Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsDedekindDomain.HeightOneSpectrum.intValuationDef Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SemilatticeSup.toMax WithZero.semilatticeSup Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Multiplicative.linearOrder Int.instLinearOrder	—	zero_add ne_of_lt le_antisymm le_trans le_of_lt le_refl le_sup_right add_zero le_sup_left Ideal.uniqueFactorizationMonoid IsDedekindDomain.HeightOneSpectrum.intValuationDef.eq_1 zero_le' Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_neg le_max_iff Int.instAddLeftMono covariant_swap_add_of_covariant_add Int.instZeroLEOneClass Int.instCharZero IsScalarTower.right Associates.le_singleton_iff Associates.prime_pow_dvd_iff_le Associates.mk_ne_zero' IsDedekindDomain.HeightOneSpectrum.associates_irreducible min_le_left min_le_right Ideal.add_mem
map_mul' 📖	mathematical	—	IsDedekindDomain.HeightOneSpectrum.intValuationDef Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing WithZero Multiplicative MulZeroClass.toMul WithZero.instMulZeroClass Multiplicative.mul	—	Ideal.uniqueFactorizationMonoid MulZeroClass.zero_mul MulZeroClass.mul_zero mul_ne_zero IsDomain.to_noZeroDivisors IsDedekindDomain.toIsDomain WithZero.exp_add IsScalarTower.left Ideal.span_singleton_mul_span_singleton Ideal.instIsTwoSided_1 neg_add Associates.count_mul Associates.mk_ne_zero' IsDedekindDomain.HeightOneSpectrum.associates_irreducible Nat.cast_add
map_one' 📖	mathematical	—	IsDedekindDomain.HeightOneSpectrum.intValuationDef AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing WithZero Multiplicative WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	Ideal.uniqueFactorizationMonoid IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_neg one_ne_zero NeZero.one IsDomain.toNontrivial IsDedekindDomain.toIsDomain Ideal.span_singleton_one Ideal.one_eq_top Associates.mk_one Associates.factors_one Ideal.instNontrivial Associates.count_zero IsDedekindDomain.HeightOneSpectrum.associates_irreducible neg_zero WithZero.exp_zero
map_zero' 📖	mathematical	—	IsDedekindDomain.HeightOneSpectrum.intValuationDef MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing WithZero Multiplicative WithZero.instZero	—	IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_pos

Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
valuation_le_one_iff_den 📖	mathematical	—	WithZero Multiplicative Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe Valuation WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing DivisionRing.toRing Field.toDivisionRing instField Valuation.instFunLike IsDedekindDomain.HeightOneSpectrum.valuation WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsDedekindDomain.HeightOneSpectrum.asIdeal AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Function.Injective.of_comp algebraMap_comp_natCast Nat.cast_injective instCharZero Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsDedekindDomain.HeightOneSpectrum.valuation_div_le_one_iff Ideal.IsPrime.notMem_of_isCoprime_of_mem IsDedekindDomain.HeightOneSpectrum.isPrime Int.cast_natCast IsCoprime.intCast IsCoprime.symm isCoprime_num_den map_intCast RingHom.instRingHomClass map_natCast num_div_den

---

← Back to Index