WithVal

📁 Source: Mathlib/Topology/Algebra/Valued/WithVal.lean

Statistics

Metric	Count
Definitions instCoeHeadWithVal, withValEquiv, ringOfIntegersWithValEquiv, orderRingIso, uniformEquiv, instCoeCompletion, WithVal, equiv, equivWithVal, instAlgebra, instAlgebra_1, instAlgebra_2, instCommRing, instField, instInhabited, instPreorder, instRing, instSMul, instValuativeRel, instValued, valuation	21
Theorems instIsDedekindDomainWithVal, instIsIntegralClosureIntWithVal, withValEquiv_apply, withValEquiv_symm_apply, ringOfIntegersWithValEquiv_apply, orderRingIso_apply, orderRingIso_symm_apply, uniformContinuous_equivWithVal, valuedCompletion_le_one_iff, exists_div_eq_of_surjective, apply_equiv, apply_symm_equiv, equivWithVal_apply, equivWithVal_symm, equivWithVal_symm_apply, instCompatibleValuation, instIsFractionRing, instIsScalarTower, instIsScalarTower_1, le_def, lt_def, valuation_equiv_symm	22
Total	43

NumberField.RingOfIntegers

Definitions

Name	Category	Theorems
instCoeHeadWithVal 📖	CompOp	—
withValEquiv 📖	CompOp	2 math math: withValEquiv_symm_apply, withValEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsDedekindDomainWithVal 📖	mathematical	—	IsDedekindDomain NumberField.RingOfIntegers WithVal DivisionRing.toRing Field.toDivisionRing WithVal.instField instCommRing	—	instIsDedekindDomain
instIsIntegralClosureIntWithVal 📖	mathematical	—	IsIntegralClosure WithVal DivisionRing.toRing Field.toDivisionRing Int.instCommRing CommRing.toCommSemiring WithVal.instCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain WithVal.instAlgebra_2 Ring.toIntAlgebra	—	—
withValEquiv_apply 📖	mathematical	—	DFunLike.coe RingEquiv NumberField.RingOfIntegers WithVal DivisionRing.toRing Field.toDivisionRing WithVal.instField Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike withValEquiv MulEquiv NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring MulEquiv.instEquivLike MulEquiv.symm MulEquivClass.toMulEquiv RingEquivClass.toMulEquivClass RingEquiv.instRingEquivClass RingEquivClass.toRingEquiv AlgEquiv Int.instCommRing Ring.toIntAlgebra CommRing.toRing AlgEquiv.instEquivLike AlgEquivClass.toRingEquivClass AlgEquiv.instAlgEquivClass IsIntegralClosure.equiv EuclideanDomain.toCommRing Field.toEuclideanDomain WithVal.instAlgebra_2 instIsIntegralClosureIntWithVal instAlgebra_1 Algebra.id Semifield.toCommSemiring Field.toSemifield instIsIntegralClosureInt	—	—
withValEquiv_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv NumberField.RingOfIntegers WithVal DivisionRing.toRing Field.toDivisionRing WithVal.instField Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm withValEquiv AlgEquiv CommRing.toCommSemiring Int.instCommRing CommSemiring.toSemiring Ring.toIntAlgebra CommRing.toRing AlgEquiv.instFunLike IsIntegralClosure.equiv EuclideanDomain.toCommRing Field.toEuclideanDomain WithVal.instAlgebra_2 instIsIntegralClosureIntWithVal instAlgebra_1 Algebra.id Semifield.toCommSemiring Field.toSemifield instIsIntegralClosureInt	—	—

Rat

Definitions

Name	Category	Theorems
ringOfIntegersWithValEquiv 📖	CompOp	1 math math: ringOfIntegersWithValEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ringOfIntegersWithValEquiv_apply 📖	mathematical	—	DFunLike.coe RingEquiv NumberField.RingOfIntegers WithVal DivisionRing.toRing instDivisionRing WithVal.instField instField Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NumberField.RingOfIntegers.instCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike ringOfIntegersWithValEquiv MulEquiv Field.toDivisionRing NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing MulEquiv.instEquivLike MulEquiv.symm MulEquivClass.toMulEquiv RingEquivClass.toMulEquivClass RingEquiv.instRingEquivClass RingEquivClass.toRingEquiv AlgEquiv Ring.toIntAlgebra CommRing.toRing AlgEquiv.instEquivLike AlgEquivClass.toRingEquivClass AlgEquiv.instAlgEquivClass IsIntegralClosure.equiv EuclideanDomain.toCommRing Field.toEuclideanDomain WithVal.instAlgebra_2 NumberField.RingOfIntegers.instIsIntegralClosureIntWithVal NumberField.RingOfIntegers.instAlgebra_1 Algebra.id Semifield.toCommSemiring Field.toSemifield NumberField.RingOfIntegers.instIsIntegralClosureInt	—	—

Valuation

Definitions

Name	Category	Theorems
instCoeCompletion 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_div_eq_of_surjective 📖	mathematical	DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing Field.toDivisionRing instFunLike	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid Units.val MonoidWithZero.toMonoid	—	map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass instValuationClass LinearOrderedCommMonoidWithZero.toZeroLeOneClass NeZero.one GroupWithZero.toNontrivial div_one

Valuation.IsEquiv

Definitions

Name	Category	Theorems
orderRingIso 📖	CompOp	2 math math: orderRingIso_apply, orderRingIso_symm_apply
uniformEquiv 📖	CompOp	1 math math: valuedCompletion_le_one_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
orderRingIso_apply 📖	mathematical	Valuation.IsEquiv LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero	DFunLike.coe OrderRingIso WithVal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing WithVal.instRing Distrib.toAdd Preorder.toLE WithVal.instPreorder EquivLike.toFunLike OrderRingIso.instEquivLike orderRingIso RingEquiv RingEquiv.instEquivLike WithVal.equivWithVal	—	—
orderRingIso_symm_apply 📖	mathematical	Valuation.IsEquiv LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero	DFunLike.coe OrderRingIso WithVal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing WithVal.instRing Distrib.toAdd Preorder.toLE WithVal.instPreorder EquivLike.toFunLike OrderRingIso.instEquivLike OrderRingIso.symm orderRingIso RingEquiv RingEquiv.instEquivLike RingEquiv.symm WithVal.equivWithVal	—	—
uniformContinuous_equivWithVal 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero DFunLike.coe Valuation Valuation.instFunLike DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid Units.val MonoidWithZero.toMonoid Valuation.IsEquiv	UniformContinuous WithVal Valued.toUniformSpace WithVal.instRing WithVal.instValued RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike WithVal.equivWithVal	—	uniformContinuous_of_continuousAt_zero Valued.toIsUniformAddGroup RingHomClass.toAddMonoidHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass Filter.HasBasis.tendsto_iff Valued.hasBasis_nhds_zero eq_zero LT.lt.ne Set.mem_setOf_eq WithVal.apply_equiv RingEquiv.apply_symm_apply lt_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE LinearOrderedCommMonoidWithZero.toMulPosStrictMono map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass NonUnitalRingHomClass.toMulHomClass RingEquivClass.toNonUnitalRingHomClass WithVal.lt_def orderRingIso_apply OrderRingIso.apply_symm_apply OrderRingIso.instRingEquivClass OrderRingIso.lt_symm_apply pos_iff
valuedCompletion_le_one_iff 📖	mathematical	Valuation.IsEquiv DivisionRing.toRing Field.toDivisionRing LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder Valuation.Completion UniformSpace.Completion.ring WithVal Valued.toUniformSpace WithVal.instValued IsTopologicalDivisionRing.toIsTopologicalRing UniformSpace.toTopologicalSpace Valued.isTopologicalDivisionRing Valued.toIsUniformAddGroup Valued.v Valued.valuedCompletion InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero UniformSpace.Completion WithVal.instRing UniformEquiv UniformSpace.Completion.uniformSpace EquivLike.toFunLike UniformEquiv.instEquivLike UniformSpace.Completion.mapEquiv uniformEquiv Valuation.exists_div_eq_of_surjective	—	UniformSpace.Completion.induction_on IsTopologicalDivisionRing.toIsTopologicalRing Valued.isTopologicalDivisionRing Valued.toIsUniformAddGroup Valuation.exists_div_eq_of_surjective Homeomorph.isClosed_setOf_iff Valued.isClopen_closedBall one_ne_zero NeZero.one GroupWithZero.toNontrivial Valued.valuedCompletion_apply UniformSpace.Completion.mapEquiv_coe le_one_iff_le_one

WithVal

Definitions

Name	Category	Theorems
equiv 📖	CompOp	12 math math: apply_symm_equiv, apply_equiv, lt_def, Padic.withValUniformEquiv_cast_apply, Padic.coe_withValRingEquiv, Padic.isUniformInducing_cast_withVal, equivWithVal_apply, Padic.coe_withValRingEquiv_symm, le_def, valuation_equiv_symm, equivWithVal_symm_apply, Padic.isDenseInducing_cast_withVal
equivWithVal 📖	CompOp	6 math math: Valuation.IsEquiv.orderRingIso_apply, Valuation.IsEquiv.uniformContinuous_equivWithVal, equivWithVal_symm, equivWithVal_apply, equivWithVal_symm_apply, Valuation.IsEquiv.orderRingIso_symm_apply
instAlgebra 📖	CompOp	1 math math: instIsFractionRing
instAlgebra_1 📖	CompOp	1 math math: instIsScalarTower_1
instAlgebra_2 📖	CompOp	5 math math: NumberField.RingOfIntegers.instIsIntegralClosureIntWithVal, NumberField.RingOfIntegers.withValEquiv_symm_apply, NumberField.RingOfIntegers.withValEquiv_apply, IsDedekindDomain.HeightOneSpectrum.adicValued_apply', Rat.ringOfIntegersWithValEquiv_apply
instCommRing 📖	CompOp	15 math math: NumberField.RingOfIntegers.instIsIntegralClosureIntWithVal, LaurentSeries.LaurentSeriesRingEquiv_def, instCompatibleValuation, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, LaurentSeries.coe_X_compare, instIsScalarTower_1, LaurentSeries.exists_powerSeries_of_memIntegers, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, instIsFractionRing, LaurentSeries.powerSeriesRingEquiv_coe_apply, Padic.coe_withValRingEquiv, Padic.coe_withValRingEquiv_symm, LaurentSeries.ratfuncAdicComplRingEquiv_apply, LaurentSeries.mem_integers_of_powerSeries
instField 📖	CompOp	51 math math: NumberField.prod_nonarchAbsVal_eq, NumberField.FinitePlace.mk_apply, Padic.withValUniformEquiv_norm_le_one_iff, IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, NumberField.FinitePlace.norm_def', IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, NumberField.FinitePlace.embedding_apply, NumberField.RingOfIntegers.withValEquiv_symm_apply, IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower', NumberField.FinitePlace.norm_embedding_eq, NumberField.RingOfIntegers.instIsDedekindDomainWithVal, LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers, IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, NumberField.FinitePlace.norm_lt_one_iff_mem, IsDedekindDomain.HeightOneSpectrum.instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, PadicInt.coe_adicCompletionIntegersEquiv_apply, NumberField.isFinitePlace_iff, NumberField.FinitePlace.coe_apply, NumberField.FinitePlace.norm_def_int, NumberField.RingOfIntegers.withValEquiv_apply, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation, IsDedekindDomain.HeightOneSpectrum.coe_mem_adicCompletionIntegers, LaurentSeries.powerSeries_ext_subring, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, LaurentSeries.powerSeriesRingEquiv_coe_apply, instIsDiscreteValuationRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, NumberField.FinitePlace.norm_eq_one_iff_notMem, Padic.isUniformInducing_cast_withVal, IsDedekindDomain.HeightOneSpectrum.adicValued_apply', Padic.coe_withValRingEquiv_symm, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, NumberField.FinitePlace.isFinitePlace, instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, NumberField.FinitePlace.norm_le_one, LaurentSeries.mem_integers_of_powerSeries, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion, IsDedekindDomain.HeightOneSpectrum.adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers, Padic.isDenseInducing_cast_withVal, NumberField.FinitePlace.norm_def, Rat.ringOfIntegersWithValEquiv_apply, IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers
instInhabited 📖	CompOp	—
instPreorder 📖	CompOp	4 math math: Valuation.IsEquiv.orderRingIso_apply, lt_def, le_def, Valuation.IsEquiv.orderRingIso_symm_apply
instRing 📖	CompOp	67 math math: IsDedekindDomain.HeightOneSpectrum.adicValued.has_uniform_continuous_const_smul', NumberField.FinitePlace.mk_apply, Padic.withValUniformEquiv_norm_le_one_iff, LaurentSeries.LaurentSeriesRingEquiv_def, IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, NumberField.FinitePlace.norm_def', IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, NumberField.FinitePlace.embedding_apply, Valuation.IsEquiv.orderRingIso_apply, Valuation.IsEquiv.valuedCompletion_le_one_iff, IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower', NumberField.FinitePlace.norm_embedding_eq, LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply, apply_symm_equiv, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, NumberField.AdeleRing.algebraMap_snd_apply, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers, apply_equiv, IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem, Valuation.IsEquiv.uniformContinuous_equivWithVal, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, equivWithVal_symm, NumberField.FinitePlace.norm_lt_one_iff_mem, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation', IsDedekindDomain.HeightOneSpectrum.instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, lt_def, PadicInt.coe_adicCompletionIntegersEquiv_apply, LaurentSeries.coe_X_compare, NumberField.FinitePlace.norm_def_int, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation, IsDedekindDomain.HeightOneSpectrum.coe_mem_adicCompletionIntegers, Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, LaurentSeries.powerSeries_ext_subring, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, LaurentSeries.powerSeriesRingEquiv_coe_apply, instIsDiscreteValuationRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, IsDedekindDomain.HeightOneSpectrum.adicValued.uniformContinuousConstSMul, Padic.withValUniformEquiv_cast_apply, Padic.coe_withValRingEquiv, NumberField.FinitePlace.norm_eq_one_iff_notMem, Padic.isUniformInducing_cast_withVal, LaurentSeries.tendsto_valuation, equivWithVal_apply, Padic.coe_withValRingEquiv_symm, NumberField.toNNReal_valued_eq_adicAbv, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletion, instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, LaurentSeries.ratfuncAdicComplRingEquiv_apply, le_def, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, valuation_equiv_symm, NumberField.FinitePlace.norm_le_one, LaurentSeries.mem_integers_of_powerSeries, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion, IsDedekindDomain.HeightOneSpectrum.adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers, equivWithVal_symm_apply, Padic.isDenseInducing_cast_withVal, NumberField.FinitePlace.norm_def, IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers, Valuation.IsEquiv.orderRingIso_symm_apply
instSMul 📖	CompOp	7 math math: IsDedekindDomain.HeightOneSpectrum.adicValued.has_uniform_continuous_const_smul', IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower', IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers, instIsScalarTower, instIsScalarTower_1, IsDedekindDomain.HeightOneSpectrum.adicValued.uniformContinuousConstSMul, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletion
instValuativeRel 📖	CompOp	1 math math: instCompatibleValuation
instValued 📖	CompOp	62 math math: IsDedekindDomain.HeightOneSpectrum.adicValued.has_uniform_continuous_const_smul', NumberField.FinitePlace.mk_apply, Padic.withValUniformEquiv_norm_le_one_iff, LaurentSeries.LaurentSeriesRingEquiv_def, IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, NumberField.FinitePlace.norm_def', IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, NumberField.FinitePlace.embedding_apply, Valuation.IsEquiv.valuedCompletion_le_one_iff, IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower', NumberField.FinitePlace.norm_embedding_eq, LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply, apply_symm_equiv, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, NumberField.AdeleRing.algebraMap_snd_apply, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers, apply_equiv, IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem, Valuation.IsEquiv.uniformContinuous_equivWithVal, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, NumberField.FinitePlace.norm_lt_one_iff_mem, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation', IsDedekindDomain.HeightOneSpectrum.instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, PadicInt.coe_adicCompletionIntegersEquiv_apply, LaurentSeries.coe_X_compare, NumberField.FinitePlace.norm_def_int, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation, IsDedekindDomain.HeightOneSpectrum.coe_mem_adicCompletionIntegers, Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, LaurentSeries.powerSeries_ext_subring, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, LaurentSeries.powerSeriesRingEquiv_coe_apply, instIsDiscreteValuationRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, IsDedekindDomain.HeightOneSpectrum.adicValued.uniformContinuousConstSMul, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective, Padic.withValUniformEquiv_cast_apply, Padic.coe_withValRingEquiv, NumberField.FinitePlace.norm_eq_one_iff_notMem, LaurentSeries.valuation_compare, Padic.isUniformInducing_cast_withVal, LaurentSeries.tendsto_valuation, Padic.coe_withValRingEquiv_symm, NumberField.toNNReal_valued_eq_adicAbv, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletion, instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, LaurentSeries.ratfuncAdicComplRingEquiv_apply, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, NumberField.FinitePlace.norm_le_one, LaurentSeries.mem_integers_of_powerSeries, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion, IsDedekindDomain.HeightOneSpectrum.adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers, Padic.isDenseInducing_cast_withVal, NumberField.FinitePlace.norm_def, IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers
valuation 📖	CompOp	2 math math: instCompatibleValuation, valuation_equiv_symm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_equiv 📖	mathematical	—	DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike RingEquiv WithVal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike equiv Valued.v instValued	—	—
apply_symm_equiv 📖	mathematical	—	DFunLike.coe Valuation WithVal LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instRing Valuation.instFunLike Valued.v instValued RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm equiv	—	—
equivWithVal_apply 📖	mathematical	—	DFunLike.coe RingEquiv WithVal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike equivWithVal RingEquiv.symm equiv	—	—
equivWithVal_symm 📖	mathematical	—	RingEquiv.symm WithVal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRing Distrib.toAdd equivWithVal	—	—
equivWithVal_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv WithVal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm equivWithVal equiv	—	—
instCompatibleValuation 📖	mathematical	—	Valuation.Compatible WithVal CommRing.toRing instCommRing LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero valuation instValuativeRel	—	Valuation.Compatible.ofValuation
instIsFractionRing 📖	mathematical	—	IsFractionRing CommRing.toCommSemiring WithVal CommRing.toRing instCommRing instAlgebra	—	—
instIsScalarTower 📖	mathematical	—	IsScalarTower WithVal instSMul	—	—
instIsScalarTower_1 📖	mathematical	—	IsScalarTower WithVal CommRing.toRing instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toSMul CommRing.toCommSemiring instCommRing Ring.toSemiring instAlgebra_1 NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	—
le_def 📖	mathematical	—	WithVal Preorder.toLE instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike equiv	—	—
lt_def 📖	mathematical	—	WithVal Preorder.toLT instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike equiv	—	—
valuation_equiv_symm 📖	mathematical	—	DFunLike.coe Valuation WithVal LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instRing Valuation.instFunLike valuation RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm equiv	—	—

(root)

Definitions

Name	Category	Theorems
WithVal 📖	CompOp	84 math math: IsDedekindDomain.HeightOneSpectrum.adicValued.has_uniform_continuous_const_smul', NumberField.prod_nonarchAbsVal_eq, NumberField.FinitePlace.mk_apply, Padic.withValUniformEquiv_norm_le_one_iff, NumberField.RingOfIntegers.instIsIntegralClosureIntWithVal, LaurentSeries.LaurentSeriesRingEquiv_def, IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, NumberField.FinitePlace.norm_def', IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, NumberField.FinitePlace.embedding_apply, Valuation.IsEquiv.orderRingIso_apply, Valuation.IsEquiv.valuedCompletion_le_one_iff, WithVal.instCompatibleValuation, NumberField.RingOfIntegers.withValEquiv_symm_apply, IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower', NumberField.FinitePlace.norm_embedding_eq, NumberField.RingOfIntegers.instIsDedekindDomainWithVal, LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply, WithVal.apply_symm_equiv, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, NumberField.AdeleRing.algebraMap_snd_apply, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers, WithVal.apply_equiv, IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem, Valuation.IsEquiv.uniformContinuous_equivWithVal, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, WithVal.equivWithVal_symm, NumberField.FinitePlace.norm_lt_one_iff_mem, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation', IsDedekindDomain.HeightOneSpectrum.instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, WithVal.lt_def, PadicInt.coe_adicCompletionIntegersEquiv_apply, NumberField.isFinitePlace_iff, LaurentSeries.coe_X_compare, WithVal.instIsScalarTower, WithVal.instIsScalarTower_1, NumberField.FinitePlace.coe_apply, NumberField.FinitePlace.norm_def_int, NumberField.RingOfIntegers.withValEquiv_apply, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation, IsDedekindDomain.HeightOneSpectrum.coe_mem_adicCompletionIntegers, Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, LaurentSeries.powerSeries_ext_subring, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, WithVal.instIsFractionRing, LaurentSeries.powerSeriesRingEquiv_coe_apply, instIsDiscreteValuationRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, IsDedekindDomain.HeightOneSpectrum.adicValued.uniformContinuousConstSMul, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective, Padic.withValUniformEquiv_cast_apply, Padic.coe_withValRingEquiv, NumberField.FinitePlace.norm_eq_one_iff_notMem, LaurentSeries.valuation_compare, Padic.isUniformInducing_cast_withVal, LaurentSeries.tendsto_valuation, IsDedekindDomain.HeightOneSpectrum.adicValued_apply', WithVal.equivWithVal_apply, Padic.coe_withValRingEquiv_symm, NumberField.toNNReal_valued_eq_adicAbv, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletion, NumberField.FinitePlace.isFinitePlace, instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, LaurentSeries.ratfuncAdicComplRingEquiv_apply, WithVal.le_def, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, WithVal.valuation_equiv_symm, NumberField.FinitePlace.norm_le_one, LaurentSeries.mem_integers_of_powerSeries, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion, IsDedekindDomain.HeightOneSpectrum.adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers, WithVal.equivWithVal_symm_apply, Padic.isDenseInducing_cast_withVal, NumberField.FinitePlace.norm_def, Rat.ringOfIntegersWithValEquiv_apply, IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers, Valuation.IsEquiv.orderRingIso_symm_apply

---

← Back to Index