WithVal

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

Statistics

Metric	Count
Definitions instCoeHeadWithVal, withValEquiv, ringOfIntegersWithValEquiv, orderRingIso, uniformEquiv, instCoeCompletion, WithVal, algEquiv, delabToVal, equiv, equivWithVal, instAlgebra, instAlgebra_1, instCommRing, instField, instInhabited, instModule, instModule_1, instPreorder, instRing, instSMul, instSMul_1, instValuativeRel, instValued, linearEquiv, map, ofVal, uniformEquiv, valuation, valueGroupEquiv, valueGroupOrderIso₀	31
Theorems instIsIntegralClosureIntWithVal, withValEquiv_apply, withValEquiv_symm_apply, ringOfIntegersWithValEquiv_apply, orderRingIso_apply, orderRingIso_symm_apply, uniformContinuous, uniformContinuous_congr, uniformContinuous_equiv, uniformContinuous_equivWithVal, uniformContinuous_equiv_symm, valuedCompletion_le_one_iff, exists_div_eq_of_surjective, restrict_exists_div_eq, algEquiv_apply, algEquiv_symm_apply, algebraMap_left_apply, algebraMap_left_injective, algebraMap_right_apply, algebraMap_right_injective, apply_equiv, apply_ofVal, apply_symm_equiv, congr_apply, congr_refl, congr_symm, congr_symm_apply, congr_trans, equivWithVal_apply, equivWithVal_symm, equivWithVal_symm_apply, equiv_apply, equiv_symm_apply, instCharZero, instCompatibleValuation, instFaithfulSMul, instFaithfulSMul_1, instFinite, instFinite_1, instIsFractionRing, instIsLocalization, instIsScalarTower, instIsScalarTower_1, instIsScalarTower_2, instNumberField, le_def, linearEquiv_apply, linearEquiv_symm_apply, lt_def, map_apply, map_comp, map_id, ofVal_add, ofVal_bijective, ofVal_div, ofVal_eq_zero, ofVal_injective, ofVal_inv, ofVal_mul, ofVal_neg, ofVal_one, ofVal_pow, ofVal_smul, ofVal_sub, ofVal_surjective, ofVal_toVal, ofVal_zero, smul_left_def, smul_right_def, strictMono_valueGroupEquiv, strictMono_valueGroupEquiv_symm, strictMono_valueGroupOrderIso₀, strictMono_valueGroupOrderIso₀_symm, toVal_add, toVal_bijective, toVal_div, toVal_eq_zero, toVal_injective, toVal_inv, toVal_mul, toVal_neg, toVal_ofVal, toVal_one, toVal_pow, toVal_smul, toVal_sub, toVal_surjective, toVal_zero, val_apply_equiv, valuation_equiv_symm, valueGroupEquiv_apply, valueGroupEquiv_symm_apply, valueGroupOrderIso₀_apply, valueGroupOrderIso₀_restrict, valueGroupOrderIso₀_symm_apply, valueGroupOrderIso₀_symm_restrict, valueGroup_eq, valued_toVal	98
Total	129

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
instIsIntegralClosureIntWithVal 📖	mathematical	—	IsIntegralClosure WithVal DivisionRing.toRing Field.toDivisionRing Int.instCommRing CommRing.toCommSemiring WithVal.instCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain WithVal.instAlgebra_1 Ring.toIntAlgebra	—	IsIntegralClosure.of_algEquiv
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 NumberField.instCommRingRingOfIntegers 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_1 instIsIntegralClosureIntWithVal instAlgebra_1 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 NumberField.instCommRingRingOfIntegers 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_1 instIsIntegralClosureIntWithVal instAlgebra_1 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.instCommRingRingOfIntegers 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_1 NumberField.RingOfIntegers.instIsIntegralClosureIntWithVal NumberField.RingOfIntegers.instAlgebra_1 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 LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero DFunLike.coe Valuation DivisionRing.toRing Field.toDivisionRing instFunLike 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
restrict_exists_div_eq 📖	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 DivisionRing.toRing Field.toDivisionRing instFunLike MonoidWithZeroHom.ValueGroup₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom ValuationClass.toMonoidWithZeroHomClass instValuationClass Semiring.toMonoidWithZero MonoidWithZeroHom.monoidWithZeroHomClass WithZero.div Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subgroup.div MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero restrict Units.val DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield WithZero.instMonoidWithZero DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup	—	ValuationClass.toMonoidWithZeroHomClass instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHom.ValueGroup₀.restrict₀_surjective map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass LinearOrderedCommMonoidWithZero.toZeroLeOneClass NeZero.one GroupWithZero.toNontrivial div_one map_zero MonoidWithZeroHomClass.toZeroHomClass MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀ StrictMono.lt_iff_lt MonoidWithZeroHom.ValueGroup₀.embedding_strictMono WithZero.pos_iff_ne_zero Units.ne_zero WithZero.instNontrivial One.instNonempty

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 WithVal.toVal WithVal.ofVal	—	—
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 WithVal.toVal WithVal.ofVal	—	—
uniformContinuous 📖	mathematical	Valuation.IsEquiv LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero	UniformContinuous Valued.toUniformSpace Valued.mk' DFunLike.coe RingHom Semiring.toNonAssocSemiring Ring.toSemiring RingHom.instFunLike RingHom.id	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass restrict uniformContinuous_of_continuousAt_zero Valued.toIsUniformAddGroup RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass Filter.HasBasis.tendsto_iff Valued.hasBasis_nhds_zero Units.ne_zero WithZero.instNontrivial One.instNonempty MonoidWithZeroHom.mem_valueGroup_iff_of_comm EquivLike.toEmbeddingLike MulEquivClass.toMonoidWithZeroHomClass OrderMonoidIso.instMulEquivClass StrictMono.lt_iff_lt OrderMonoidIso.strictMono Units.val_mk0 orderMonoidIso_spec
uniformContinuous_congr 📖	mathematical	Valuation.IsEquiv LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero	UniformContinuous WithVal Valued.toUniformSpace WithVal.instRing WithVal.instValued DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike WithVal.congr RingEquiv.refl	—	RingEquiv.ext_iff uniformContinuous_equiv uniformContinuous_equiv_symm uniformContinuous UniformContinuous.comp
uniformContinuous_equiv 📖	mathematical	Valued.v Valuation.IsEquiv LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero	UniformContinuous WithVal Valued.toUniformSpace WithVal.instRing WithVal.instValued DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike WithVal.equiv	—	uniformContinuous_of_continuousAt_zero Valued.toIsUniformAddGroup RingHomClass.toAddMonoidHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass Filter.HasBasis.tendsto_iff Valued.hasBasis_nhds_zero Valuation.exists_div_eq_of_unit Iff.ne eq_zero LT.lt.ne' pos_iff restrict WithVal.equiv_apply Set.mem_setOf_eq lt_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE LinearOrderedCommMonoidWithZero.toMulPosStrictMono Valuation.restrict_pos_iff map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass WithVal.lt_def WithVal.ofVal_mul WithVal.toVal_mul orderRingIso_apply OrderRingIso.lt_symm_apply Valuation.restrict_lt_iff
uniformContinuous_equivWithVal 📖	mathematical	Valuation.IsEquiv LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero	UniformContinuous WithVal Valued.toUniformSpace WithVal.instRing WithVal.instValued DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike WithVal.congr RingEquiv.refl	—	uniformContinuous_congr
uniformContinuous_equiv_symm 📖	mathematical	Valued.v Valuation.IsEquiv LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero	UniformContinuous WithVal Valued.toUniformSpace WithVal.instRing WithVal.instValued DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm WithVal.equiv	—	uniformContinuous_of_continuousAt_zero Valued.toIsUniformAddGroup RingHomClass.toAddMonoidHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass Filter.HasBasis.tendsto_iff Valued.hasBasis_nhds_zero Valuation.exists_div_eq_of_unit restrict Iff.ne eq_zero LT.lt.ne' lt_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE LinearOrderedCommMonoidWithZero.toMulPosStrictMono Valuation.restrict_pos_iff map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass WithVal.lt_def orderRingIso_apply lt_iff_lt Valuation.restrict_lt_iff pos_iff
valuedCompletion_le_one_iff 📖	mathematical	Valuation.IsEquiv DivisionRing.toRing Field.toDivisionRing LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation Valuation.Completion DivisionRing.toRing Field.toDivisionRing UniformSpace.Completion.ring WithVal WithVal.instField Valued.toUniformSpace WithVal.instValued IsTopologicalDivisionRing.toIsTopologicalRing UniformSpace.toTopologicalSpace Valued.isTopologicalDivisionRing Valued.toIsUniformAddGroup Valuation.instFunLike 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	—	UniformSpace.Completion.induction_on IsTopologicalDivisionRing.toIsTopologicalRing Valued.isTopologicalDivisionRing Valued.toIsUniformAddGroup ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass Valuation.restrict_le_one_iff Homeomorph.isClosed_setOf_iff Valued.isClopen_closedBall one_ne_zero NeZero.one WithZero.instNontrivial One.instNonempty Valued.valuedCompletion_apply UniformSpace.Completion.mapEquiv_coe le_one_iff_le_one

WithVal

Definitions

Name	Category	Theorems
algEquiv 📖	CompOp	2 math math: algEquiv_symm_apply, algEquiv_apply
delabToVal 📖	CompOp	—
equiv 📖	CompOp	25 math math: NumberField.FinitePlace.embedding_apply, NumberField.HeightOneSpectrum.NumberField.toNNReal_valued_eq_adicAbv, Valuation.IsEquiv.uniformContinuous_equiv, val_apply_equiv, NumberField.AdeleRing.algebraMap_snd_apply, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply, IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem, equiv_symm_apply, equiv_apply, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation', LaurentSeries.coe_X_compare, LaurentSeries.continuous_coe', Padic.withValUniformEquiv_cast_apply, Padic.coe_withValRingEquiv, Padic.isUniformInducing_cast_withVal, LaurentSeries.tendsto_valuation, Valuation.IsEquiv.uniformContinuous_equiv_symm, IsDedekindDomain.HeightOneSpectrum.adicValued_apply', equivWithVal_apply, Padic.coe_withValRingEquiv_symm, NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbv, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion, equivWithVal_symm_apply, Padic.isDenseInducing_cast_withVal, LaurentSeries.uniformContinuous_withVal_equiv
equivWithVal 📖	CompOp	—
instAlgebra 📖	CompOp	3 math math: algebraMap_left_apply, algebraMap_left_injective, instIsFractionRing
instAlgebra_1 📖	CompOp	9 math math: NumberField.RingOfIntegers.instIsIntegralClosureIntWithVal, NumberField.RingOfIntegers.withValEquiv_symm_apply, algEquiv_symm_apply, NumberField.RingOfIntegers.withValEquiv_apply, algEquiv_apply, instIsLocalization, algebraMap_right_injective, Rat.ringOfIntegersWithValEquiv_apply, algebraMap_right_apply
instCommRing 📖	CompOp	31 math math: NumberField.RingOfIntegers.instIsIntegralClosureIntWithVal, LaurentSeries.LaurentSeriesRingEquiv_def, IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, NumberField.HeightOneSpectrum.rankOne_hom'_def, instCompatibleValuation, IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower', IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers, NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def, algebraMap_left_apply, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, IsDedekindDomain.HeightOneSpectrum.instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, PadicInt.coe_adicCompletionIntegersEquiv_apply, LaurentSeries.coe_X_compare, LaurentSeries.exists_powerSeries_of_memIntegers, algebraMap_left_injective, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, LaurentSeries.powerSeries_ext_subring, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, instIsFractionRing, LaurentSeries.powerSeriesRingEquiv_coe_apply, instIsLocalization, Padic.coe_withValRingEquiv, Padic.coe_withValRingEquiv_symm, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, LaurentSeries.ratfuncAdicComplRingEquiv_apply, LaurentSeries.mem_integers_of_powerSeries
instField 📖	CompOp	69 math math: NumberField.FinitePlace.mk_apply, Padic.withValUniformEquiv_norm_le_one_iff, IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap, toVal_inv, IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, NumberField.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicCompletionV, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, NumberField.FinitePlace.norm_def', IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, NumberField.FinitePlace.embedding_apply, NumberField.HeightOneSpectrum.rankOne_hom'_def, Valuation.IsEquiv.valuedCompletion_le_one_iff, NumberField.RingOfIntegers.withValEquiv_symm_apply, IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower', NumberField.FinitePlace.norm_embedding_eq, LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, NumberField.FinitePlace.norm_embedding, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers, IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem, NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def, IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers_1, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, NumberField.FinitePlace.norm_lt_one_iff_mem, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation', instNumberField, IsDedekindDomain.HeightOneSpectrum.instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply, PadicInt.coe_adicCompletionIntegersEquiv_apply, ofVal_inv, NumberField.HeightOneSpectrum.embedding_mul_absNorm, ofVal_div, NumberField.FinitePlace.equivHeightOneSpectrum_symm_apply, NumberField.FinitePlace.norm_def_int, NumberField.RingOfIntegers.withValEquiv_apply, toVal_div, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation, IsDedekindDomain.HeightOneSpectrum.coe_mem_adicCompletionIntegers, LaurentSeries.powerSeries_ext_subring, NumberField.HeightOneSpectrum.instFiniteAdicCompletionRingOfIntegers, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, LaurentSeries.powerSeriesRingEquiv_coe_apply, instIsDiscreteValuationRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective, NumberField.FinitePlace.norm_eq_one_iff_notMem, LaurentSeries.valuation_compare, Padic.isUniformInducing_cast_withVal, LaurentSeries.tendsto_valuation, Padic.coe_withValRingEquiv_symm, IsDedekindDomain.HeightOneSpectrum.adicCompletion_valueGroup_eq, LaurentSeries.comparePkg_eq_extension, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, NumberField.FinitePlace.norm_embedding', NumberField.FinitePlace.norm_le_one, LaurentSeries.mem_integers_of_powerSeries, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion, IsDedekindDomain.HeightOneSpectrum.adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers, NumberField.FinitePlace.norm_embedding_int, Padic.isDenseInducing_cast_withVal, NumberField.FinitePlace.norm_def, Rat.ringOfIntegersWithValEquiv_apply, IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers
instInhabited 📖	CompOp	—
instModule 📖	CompOp	1 math math: instFinite
instModule_1 📖	CompOp	3 math math: linearEquiv_apply, linearEquiv_symm_apply, instFinite_1
instPreorder 📖	CompOp	4 math math: Valuation.IsEquiv.orderRingIso_apply, lt_def, le_def, Valuation.IsEquiv.orderRingIso_symm_apply
instRing 📖	CompOp	137 math math: ofVal_add, map_comp, IsDedekindDomain.HeightOneSpectrum.adicValued.has_uniform_continuous_const_smul', valued_toVal, valueGroupOrderIso₀_symm_apply, NumberField.FinitePlace.mk_apply, Padic.withValUniformEquiv_norm_le_one_iff, valueGroup_eq, IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap, toVal_zero, LaurentSeries.LaurentSeriesRingEquiv_def, IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, NumberField.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicCompletionV, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, NumberField.FinitePlace.norm_def', valueGroupOrderIso₀_restrict, IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, apply_ofVal, instCharZero, NumberField.FinitePlace.embedding_apply, valueGroupOrderIso₀_apply, NumberField.HeightOneSpectrum.NumberField.toNNReal_valued_eq_adicAbv, Valuation.IsEquiv.orderRingIso_apply, NumberField.HeightOneSpectrum.rankOne_hom'_def, valueGroupEquiv_symm_apply, Valuation.IsEquiv.valuedCompletion_le_one_iff, ofVal_mul, IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower', Valuation.IsEquiv.uniformContinuous_equiv, NumberField.FinitePlace.norm_embedding_eq, LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, ofVal_one, NumberField.FinitePlace.norm_embedding, apply_symm_equiv, congr_symm_apply, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, val_apply_equiv, NumberField.AdeleRing.algebraMap_snd_apply, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers, apply_equiv, IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem, linearEquiv_apply, algEquiv_symm_apply, NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def, equiv_symm_apply, Valuation.IsEquiv.uniformContinuous_equivWithVal, IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers_1, toVal_mul, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, strictMono_valueGroupOrderIso₀, equivWithVal_symm, NumberField.FinitePlace.norm_lt_one_iff_mem, strictMono_valueGroupOrderIso₀_symm, valueGroupEquiv_apply, equiv_apply, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation', Valuation.IsEquiv.uniformContinuous_congr, IsDedekindDomain.HeightOneSpectrum.instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, toVal_sub, ofVal_zero, NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply, instFinite, PadicInt.coe_adicCompletionIntegersEquiv_apply, map_id, linearEquiv_symm_apply, LaurentSeries.coe_X_compare, NumberField.HeightOneSpectrum.embedding_mul_absNorm, toVal_neg, LaurentSeries.exists_powerSeries_of_memIntegers, LaurentSeries.continuous_coe', NumberField.FinitePlace.equivHeightOneSpectrum_symm_apply, NumberField.FinitePlace.norm_def_int, toVal_pow, ofVal_sub, toVal_one, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation, IsDedekindDomain.HeightOneSpectrum.coe_mem_adicCompletionIntegers, strictMono_valueGroupEquiv_symm, Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, LaurentSeries.valuation_LaurentSeries_equal_extension, ofVal_pow, LaurentSeries.LaurentSeries_coe, LaurentSeries.powerSeries_ext_subring, NumberField.HeightOneSpectrum.instFiniteAdicCompletionRingOfIntegers, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, instFinite_1, LaurentSeries.powerSeriesRingEquiv_coe_apply, instIsDiscreteValuationRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, toVal_eq_zero, congr_apply, IsDedekindDomain.HeightOneSpectrum.adicValued.uniformContinuousConstSMul, map_apply, algEquiv_apply, ofVal_neg, Padic.withValUniformEquiv_cast_apply, Padic.coe_withValRingEquiv, NumberField.FinitePlace.norm_eq_one_iff_notMem, valueGroupOrderIso₀_symm_restrict, toVal_add, LaurentSeries.valuation_compare, Padic.isUniformInducing_cast_withVal, LaurentSeries.tendsto_valuation, congr_symm, Valuation.IsEquiv.uniformContinuous_equiv_symm, IsDedekindDomain.HeightOneSpectrum.adicValued_apply', equivWithVal_apply, Padic.coe_withValRingEquiv_symm, IsDedekindDomain.HeightOneSpectrum.adicCompletion_valueGroup_eq, LaurentSeries.comparePkg_eq_extension, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletion, congr_refl, instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, LaurentSeries.ratfuncAdicComplRingEquiv_apply, ofVal_eq_zero, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, valuation_equiv_symm, NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbv, NumberField.FinitePlace.norm_embedding', NumberField.FinitePlace.norm_le_one, LaurentSeries.mem_integers_of_powerSeries, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion, strictMono_valueGroupEquiv, IsDedekindDomain.HeightOneSpectrum.adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers, algebraMap_right_injective, equivWithVal_symm_apply, NumberField.FinitePlace.norm_embedding_int, Padic.isDenseInducing_cast_withVal, congr_trans, LaurentSeries.uniformContinuous_withVal_equiv, algebraMap_right_apply, IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers, Valuation.IsEquiv.orderRingIso_symm_apply
instSMul 📖	CompOp	4 math math: instFaithfulSMul, instIsScalarTower, instIsScalarTower_2, smul_left_def
instSMul_1 📖	CompOp	11 math math: IsDedekindDomain.HeightOneSpectrum.adicValued.has_uniform_continuous_const_smul', IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower', IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers, instIsScalarTower_1, instIsScalarTower_2, instFaithfulSMul_1, toVal_smul, ofVal_smul, smul_right_def, IsDedekindDomain.HeightOneSpectrum.adicValued.uniformContinuousConstSMul, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletion
instValuativeRel 📖	CompOp	1 math math: instCompatibleValuation
instValued 📖	CompOp	98 math math: IsDedekindDomain.HeightOneSpectrum.adicValued.has_uniform_continuous_const_smul', valued_toVal, valueGroupOrderIso₀_symm_apply, NumberField.FinitePlace.mk_apply, Padic.withValUniformEquiv_norm_le_one_iff, valueGroup_eq, IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap, LaurentSeries.LaurentSeriesRingEquiv_def, IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, NumberField.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicCompletionV, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, NumberField.FinitePlace.norm_def', valueGroupOrderIso₀_restrict, IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, apply_ofVal, NumberField.FinitePlace.embedding_apply, valueGroupOrderIso₀_apply, NumberField.HeightOneSpectrum.NumberField.toNNReal_valued_eq_adicAbv, NumberField.HeightOneSpectrum.rankOne_hom'_def, valueGroupEquiv_symm_apply, Valuation.IsEquiv.valuedCompletion_le_one_iff, IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower', Valuation.IsEquiv.uniformContinuous_equiv, NumberField.FinitePlace.norm_embedding_eq, LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, NumberField.FinitePlace.norm_embedding, apply_symm_equiv, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, val_apply_equiv, NumberField.AdeleRing.algebraMap_snd_apply, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers, apply_equiv, IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem, NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def, Valuation.IsEquiv.uniformContinuous_equivWithVal, IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers_1, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, strictMono_valueGroupOrderIso₀, NumberField.FinitePlace.norm_lt_one_iff_mem, strictMono_valueGroupOrderIso₀_symm, valueGroupEquiv_apply, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation', Valuation.IsEquiv.uniformContinuous_congr, IsDedekindDomain.HeightOneSpectrum.instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply, PadicInt.coe_adicCompletionIntegersEquiv_apply, LaurentSeries.coe_X_compare, NumberField.HeightOneSpectrum.embedding_mul_absNorm, LaurentSeries.exists_powerSeries_of_memIntegers, LaurentSeries.continuous_coe', NumberField.FinitePlace.equivHeightOneSpectrum_symm_apply, NumberField.FinitePlace.norm_def_int, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation, IsDedekindDomain.HeightOneSpectrum.coe_mem_adicCompletionIntegers, strictMono_valueGroupEquiv_symm, Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, LaurentSeries.valuation_LaurentSeries_equal_extension, LaurentSeries.LaurentSeries_coe, LaurentSeries.powerSeries_ext_subring, NumberField.HeightOneSpectrum.instFiniteAdicCompletionRingOfIntegers, 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, valueGroupOrderIso₀_symm_restrict, LaurentSeries.valuation_compare, Padic.isUniformInducing_cast_withVal, LaurentSeries.tendsto_valuation, Valuation.IsEquiv.uniformContinuous_equiv_symm, Padic.coe_withValRingEquiv_symm, IsDedekindDomain.HeightOneSpectrum.adicCompletion_valueGroup_eq, LaurentSeries.comparePkg_eq_extension, 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, NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbv, NumberField.FinitePlace.norm_embedding', NumberField.FinitePlace.norm_le_one, LaurentSeries.mem_integers_of_powerSeries, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion, strictMono_valueGroupEquiv, IsDedekindDomain.HeightOneSpectrum.adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers, NumberField.FinitePlace.norm_embedding_int, Padic.isDenseInducing_cast_withVal, LaurentSeries.uniformContinuous_withVal_equiv, NumberField.FinitePlace.norm_def, IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers
linearEquiv 📖	CompOp	2 math math: linearEquiv_apply, linearEquiv_symm_apply
map 📖	CompOp	3 math math: map_comp, map_id, map_apply
ofVal 📖	CompOp	32 math math: ofVal_add, ofVal_toVal, valueGroupOrderIso₀_restrict, apply_ofVal, toVal_ofVal, Valuation.IsEquiv.orderRingIso_apply, ofVal_mul, ofVal_one, ofVal_injective, congr_symm_apply, apply_equiv, linearEquiv_apply, algebraMap_left_apply, equiv_apply, ofVal_zero, lt_def, ofVal_inv, ofVal_div, ofVal_sub, ofVal_pow, ofVal_smul, ofVal_surjective, smul_right_def, ofVal_bijective, congr_apply, map_apply, algEquiv_apply, ofVal_neg, ofVal_eq_zero, le_def, smul_left_def, Valuation.IsEquiv.orderRingIso_symm_apply
uniformEquiv 📖	CompOp	—
valuation 📖	CompOp	2 math math: instCompatibleValuation, valuation_equiv_symm
valueGroupEquiv 📖	CompOp	6 math math: valueGroupOrderIso₀_symm_apply, valueGroupOrderIso₀_apply, valueGroupEquiv_symm_apply, valueGroupEquiv_apply, strictMono_valueGroupEquiv_symm, strictMono_valueGroupEquiv
valueGroupOrderIso₀ 📖	CompOp	6 math math: valueGroupOrderIso₀_symm_apply, valueGroupOrderIso₀_restrict, valueGroupOrderIso₀_apply, strictMono_valueGroupOrderIso₀, strictMono_valueGroupOrderIso₀_symm, valueGroupOrderIso₀_symm_restrict

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv WithVal Ring.toSemiring instRing instAlgebra_1 AlgEquiv.instFunLike algEquiv ofVal	—	—
algEquiv_symm_apply 📖	mathematical	—	DFunLike.coe AlgEquiv WithVal Ring.toSemiring instRing instAlgebra_1 AlgEquiv.instFunLike AlgEquiv.symm algEquiv toVal	—	—
algebraMap_left_apply 📖	mathematical	—	DFunLike.coe RingHom WithVal CommRing.toRing Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.instFunLike algebraMap instAlgebra ofVal	—	—
algebraMap_left_injective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	WithVal CommRing.toRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.instFunLike algebraMap instAlgebra	—	ofVal_injective
algebraMap_right_apply 📖	mathematical	—	DFunLike.coe RingHom WithVal Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring instRing RingHom.instFunLike algebraMap instAlgebra_1 toVal	—	—
algebraMap_right_injective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap	WithVal DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring instRing RingHom.instFunLike algebraMap instAlgebra_1	—	toVal_injective
apply_equiv 📖	mathematical	—	DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike ofVal WithVal instRing Valued.v instValued	—	apply_ofVal
apply_ofVal 📖	mathematical	—	DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike ofVal WithVal instRing Valued.v instValued	—	—
apply_symm_equiv 📖	mathematical	—	DFunLike.coe Valuation WithVal LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instRing Valuation.instFunLike Valued.v instValued toVal	—	valued_toVal
congr_apply 📖	mathematical	—	DFunLike.coe RingEquiv WithVal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike congr toVal ofVal	—	—
congr_refl 📖	mathematical	—	congr RingEquiv.refl Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toAdd WithVal instRing	—	—
congr_symm 📖	mathematical	—	RingEquiv.symm WithVal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRing Distrib.toAdd congr	—	—
congr_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 congr toVal ofVal	—	—
congr_trans 📖	mathematical	—	congr RingEquiv.trans Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toAdd WithVal instRing	—	—
equivWithVal_apply 📖	mathematical	—	DFunLike.coe RingEquiv WithVal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike congr RingEquiv.refl RingEquiv.symm equiv	—	—
equivWithVal_symm 📖	mathematical	—	RingEquiv.symm WithVal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRing Distrib.toAdd congr RingEquiv.refl	—	—
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 congr RingEquiv.refl equiv	—	—
equiv_apply 📖	mathematical	—	DFunLike.coe RingEquiv WithVal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike equiv ofVal	—	—
equiv_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 equiv toVal	—	—
instCharZero 📖	mathematical	—	CharZero WithVal AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instRing	—	CharZero.of_addMonoidHom RingEquiv.injective
instCompatibleValuation 📖	mathematical	—	Valuation.Compatible WithVal CommRing.toRing instCommRing LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero valuation instValuativeRel	—	Valuation.Compatible.ofValuation
instFaithfulSMul 📖	mathematical	—	FaithfulSMul WithVal instSMul	—	ofVal_injective FaithfulSMul.eq_of_smul_eq_smul
instFaithfulSMul_1 📖	mathematical	—	FaithfulSMul WithVal instSMul_1	—	FaithfulSMul.eq_of_smul_eq_smul
instFinite 📖	mathematical	—	Module.Finite WithVal Ring.toSemiring instRing instModule	—	Module.Finite.of_restrictScalars_finite instIsScalarTower_2 IsScalarTower.left
instFinite_1 📖	mathematical	—	Module.Finite WithVal Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRing instModule_1	—	Module.Finite.equiv RingHomInvPair.ids
instIsFractionRing 📖	mathematical	—	IsFractionRing WithVal CommRing.toRing CommRing.toCommSemiring instCommRing instAlgebra CommSemiring.toSemiring	—	IsFractionRing.of_ringEquiv_left
instIsLocalization 📖	mathematical	—	IsLocalization WithVal CommRing.toRing CommRing.toCommSemiring instCommRing instAlgebra_1	—	IsLocalization.isLocalization_iff_of_algEquiv
instIsScalarTower 📖	mathematical	—	IsScalarTower WithVal instSMul	—	smul_assoc
instIsScalarTower_1 📖	mathematical	—	IsScalarTower WithVal instSMul_1	—	Equiv.isScalarTower
instIsScalarTower_2 📖	mathematical	—	IsScalarTower WithVal instSMul_1 instSMul	—	smul_assoc
instNumberField 📖	mathematical	—	NumberField WithVal DivisionRing.toRing Field.toDivisionRing instField	—	instCharZero NumberField.to_charZero instFinite_1 NumberField.to_finiteDimensional
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 ofVal	—	—
linearEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids WithVal NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRing instModule_1 EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv linearEquiv ofVal	—	RingHomInvPair.ids
linearEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids WithVal NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRing instModule_1 EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm linearEquiv toVal	—	RingHomInvPair.ids
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 ofVal	—	—
map_apply 📖	mathematical	—	DFunLike.coe RingHom WithVal Semiring.toNonAssocSemiring Ring.toSemiring instRing RingHom.instFunLike map toVal ofVal	—	—
map_comp 📖	mathematical	—	map RingHom.comp Semiring.toNonAssocSemiring Ring.toSemiring WithVal instRing	—	—
map_id 📖	mathematical	—	map RingHom.id Semiring.toNonAssocSemiring Ring.toSemiring WithVal instRing	—	—
ofVal_add 📖	mathematical	—	ofVal WithVal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRing	—	—
ofVal_bijective 📖	mathematical	—	Function.Bijective WithVal ofVal	—	ofVal_injective ofVal_surjective
ofVal_div 📖	mathematical	—	ofVal DivisionRing.toRing Field.toDivisionRing WithVal DivInvMonoid.toDiv DivisionRing.toDivInvMonoid instField	—	—
ofVal_eq_zero 📖	mathematical	—	ofVal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing WithVal instRing	—	ofVal_injective
ofVal_injective 📖	mathematical	—	WithVal ofVal	—	toVal_ofVal
ofVal_inv 📖	mathematical	—	ofVal DivisionRing.toRing Field.toDivisionRing WithVal InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield instField	—	—
ofVal_mul 📖	mathematical	—	ofVal WithVal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRing	—	—
ofVal_neg 📖	mathematical	—	ofVal WithVal NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup instRing	—	—
ofVal_one 📖	mathematical	—	ofVal WithVal AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instRing	—	—
ofVal_pow 📖	mathematical	—	ofVal WithVal Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring instRing	—	—
ofVal_smul 📖	mathematical	—	ofVal WithVal instSMul_1	—	—
ofVal_sub 📖	mathematical	—	ofVal WithVal SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instRing	—	—
ofVal_surjective 📖	mathematical	—	WithVal ofVal	—	ofVal_toVal
ofVal_toVal 📖	mathematical	—	ofVal toVal	—	—
ofVal_zero 📖	mathematical	—	ofVal WithVal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRing	—	—
smul_left_def 📖	mathematical	—	WithVal instSMul ofVal	—	—
smul_right_def 📖	mathematical	—	WithVal instSMul_1 toVal ofVal	—	—
strictMono_valueGroupEquiv 📖	mathematical	—	StrictMono Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup WithVal Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instRing Valuation.instFunLike Valued.v instValued Semiring.toMonoidWithZero Ring.toSemiring ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike valueGroupEquiv	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass
strictMono_valueGroupEquiv_symm 📖	mathematical	—	StrictMono Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike Semiring.toMonoidWithZero Ring.toSemiring ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass WithVal instRing Valued.v instValued Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm valueGroupEquiv	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass
strictMono_valueGroupOrderIso₀ 📖	mathematical	—	StrictMono MonoidWithZeroHom.ValueGroup₀ WithVal Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instRing Valuation.instFunLike Valued.v instValued Semiring.toMonoidWithZero Ring.toSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe OrderMonoidIso MulZeroClass.toMul WithZero.instMulZeroClass Subgroup.mul EquivLike.toFunLike OrderMonoidIso.instEquivLike valueGroupOrderIso₀	—	WithZero.map'_strictMono ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass strictMono_valueGroupEquiv
strictMono_valueGroupOrderIso₀_symm 📖	mathematical	—	StrictMono MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike Semiring.toMonoidWithZero Ring.toSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass WithVal instRing Valued.v instValued WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe OrderMonoidIso MulZeroClass.toMul WithZero.instMulZeroClass Subgroup.mul EquivLike.toFunLike OrderMonoidIso.instEquivLike OrderMonoidIso.symm valueGroupOrderIso₀	—	WithZero.map'_strictMono ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass strictMono_valueGroupEquiv_symm
toVal_add 📖	mathematical	—	toVal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing WithVal instRing	—	—
toVal_bijective 📖	mathematical	—	Function.Bijective WithVal toVal	—	toVal_injective toVal_surjective
toVal_div 📖	mathematical	—	toVal DivisionRing.toRing Field.toDivisionRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid WithVal instField	—	—
toVal_eq_zero 📖	mathematical	—	toVal WithVal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRing	—	toVal_injective
toVal_injective 📖	mathematical	—	WithVal toVal	—	ofVal_toVal
toVal_inv 📖	mathematical	—	toVal DivisionRing.toRing Field.toDivisionRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield WithVal instField	—	—
toVal_mul 📖	mathematical	—	toVal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing WithVal instRing	—	—
toVal_neg 📖	mathematical	—	toVal NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup WithVal instRing	—	—
toVal_ofVal 📖	mathematical	—	toVal ofVal	—	—
toVal_one 📖	mathematical	—	toVal AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne WithVal instRing	—	—
toVal_pow 📖	mathematical	—	toVal Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring WithVal instRing	—	—
toVal_smul 📖	mathematical	—	toVal WithVal instSMul_1	—	—
toVal_sub 📖	mathematical	—	toVal SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne WithVal instRing	—	—
toVal_surjective 📖	mathematical	—	WithVal toVal	—	toVal_ofVal
toVal_zero 📖	mathematical	—	toVal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing WithVal instRing	—	—
val_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	—	—
valuation_equiv_symm 📖	mathematical	—	DFunLike.coe Valuation WithVal LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instRing Valuation.instFunLike valuation toVal	—	—
valueGroupEquiv_apply 📖	mathematical	—	DFunLike.coe MulEquiv Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup WithVal Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instRing Valuation.instFunLike Valued.v instValued Semiring.toMonoidWithZero Ring.toSemiring ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike valueGroupEquiv Set Set.instMembership SetLike.coe Equiv.refl	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass
valueGroupEquiv_symm_apply 📖	mathematical	—	DFunLike.coe MulEquiv Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike Semiring.toMonoidWithZero Ring.toSemiring ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass WithVal instRing Valued.v instValued Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm valueGroupEquiv Set Set.instMembership SetLike.coe Equiv.refl	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass
valueGroupOrderIso₀_apply 📖	mathematical	—	DFunLike.coe OrderMonoidIso MonoidWithZeroHom.ValueGroup₀ WithVal Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instRing Valuation.instFunLike Valued.v instValued Semiring.toMonoidWithZero Ring.toSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder MulZeroClass.toMul WithZero.instMulZeroClass Subgroup.mul EquivLike.toFunLike OrderMonoidIso.instEquivLike valueGroupOrderIso₀ MonoidWithZeroHom WithZero WithZero.instMulZeroOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidWithZeroHom.funLike WithZero.map' MonoidHomClass.toMonoidHom MulEquiv MulOneClass.toMulOne MulEquiv.instEquivLike valueGroupEquiv	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass
valueGroupOrderIso₀_restrict 📖	mathematical	—	DFunLike.coe OrderMonoidIso MonoidWithZeroHom.ValueGroup₀ WithVal Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instRing Valuation.instFunLike Valued.v instValued Semiring.toMonoidWithZero Ring.toSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder MulZeroClass.toMul WithZero.instMulZeroClass Subgroup.mul EquivLike.toFunLike OrderMonoidIso.instEquivLike valueGroupOrderIso₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict ofVal	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass Valuation.restrict_def map_zero MonoidWithZeroHomClass.toZeroHomClass
valueGroupOrderIso₀_symm_apply 📖	mathematical	—	DFunLike.coe OrderMonoidIso MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike Semiring.toMonoidWithZero Ring.toSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass WithVal instRing Valued.v instValued WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder MulZeroClass.toMul WithZero.instMulZeroClass Subgroup.mul EquivLike.toFunLike OrderMonoidIso.instEquivLike OrderMonoidIso.symm valueGroupOrderIso₀ MonoidWithZeroHom WithZero WithZero.instMulZeroOneClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidWithZeroHom.funLike WithZero.map' MonoidHomClass.toMonoidHom MulEquiv MulOneClass.toMulOne MulEquiv.instEquivLike MulEquiv.symm valueGroupEquiv	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass
valueGroupOrderIso₀_symm_restrict 📖	mathematical	—	DFunLike.coe OrderMonoidIso MonoidWithZeroHom.ValueGroup₀ Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike Semiring.toMonoidWithZero Ring.toSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass WithVal instRing Valued.v instValued WithZero.instPreorder Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subtype.preorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder MulZeroClass.toMul WithZero.instMulZeroClass Subgroup.mul EquivLike.toFunLike OrderMonoidIso.instEquivLike OrderMonoidIso.symm valueGroupOrderIso₀ MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidWithZeroHom MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHom.ValueGroup₀.instLinearOrderedCommGroupWithZero Valuation.restrict toVal	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass Valuation.restrict_def map_zero MonoidWithZeroHomClass.toZeroHomClass
valueGroup_eq 📖	mathematical	—	MonoidWithZeroHom.valueGroup WithVal Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instRing Valuation.instFunLike Valued.v instValued Semiring.toMonoidWithZero Ring.toSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Function.Surjective.range_comp ofVal_surjective
valued_toVal 📖	mathematical	—	DFunLike.coe Valuation WithVal LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instRing Valuation.instFunLike Valued.v instValued toVal	—	—

(root)

Definitions

Name	Category	Theorems
WithVal 📖	CompData	171 math math: WithVal.ofVal_add, WithVal.map_comp, IsDedekindDomain.HeightOneSpectrum.adicValued.has_uniform_continuous_const_smul', WithVal.valued_toVal, WithVal.valueGroupOrderIso₀_symm_apply, NumberField.FinitePlace.mk_apply, Padic.withValUniformEquiv_norm_le_one_iff, WithVal.valueGroup_eq, NumberField.RingOfIntegers.instIsIntegralClosureIntWithVal, IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap, WithVal.toVal_inv, WithVal.toVal_zero, WithVal.instFaithfulSMul, LaurentSeries.LaurentSeriesRingEquiv_def, IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, NumberField.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicCompletionV, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, NumberField.FinitePlace.norm_def', WithVal.valueGroupOrderIso₀_restrict, IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, WithVal.apply_ofVal, WithVal.toVal_bijective, WithVal.instCharZero, NumberField.FinitePlace.embedding_apply, WithVal.valueGroupOrderIso₀_apply, NumberField.HeightOneSpectrum.NumberField.toNNReal_valued_eq_adicAbv, Valuation.IsEquiv.orderRingIso_apply, NumberField.HeightOneSpectrum.rankOne_hom'_def, WithVal.valueGroupEquiv_symm_apply, Valuation.IsEquiv.valuedCompletion_le_one_iff, WithVal.instCompatibleValuation, WithVal.ofVal_mul, NumberField.RingOfIntegers.withValEquiv_symm_apply, IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower', Valuation.IsEquiv.uniformContinuous_equiv, NumberField.FinitePlace.norm_embedding_eq, LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, WithVal.toVal_surjective, WithVal.ofVal_one, WithVal.ofVal_injective, NumberField.FinitePlace.norm_embedding, WithVal.apply_symm_equiv, WithVal.congr_symm_apply, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, WithVal.val_apply_equiv, NumberField.AdeleRing.algebraMap_snd_apply, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers, WithVal.apply_equiv, IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem, WithVal.linearEquiv_apply, WithVal.algEquiv_symm_apply, NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def, WithVal.equiv_symm_apply, Valuation.IsEquiv.uniformContinuous_equivWithVal, IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers_1, WithVal.algebraMap_left_apply, WithVal.toVal_mul, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, WithVal.strictMono_valueGroupOrderIso₀, WithVal.equivWithVal_symm, NumberField.FinitePlace.norm_lt_one_iff_mem, WithVal.strictMono_valueGroupOrderIso₀_symm, WithVal.valueGroupEquiv_apply, WithVal.equiv_apply, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation', Valuation.IsEquiv.uniformContinuous_congr, WithVal.instNumberField, IsDedekindDomain.HeightOneSpectrum.instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, WithVal.toVal_sub, WithVal.ofVal_zero, NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply, WithVal.lt_def, WithVal.instFinite, PadicInt.coe_adicCompletionIntegersEquiv_apply, WithVal.map_id, WithVal.linearEquiv_symm_apply, WithVal.ofVal_inv, LaurentSeries.coe_X_compare, NumberField.HeightOneSpectrum.embedding_mul_absNorm, WithVal.ofVal_div, WithVal.instIsScalarTower, WithVal.instIsScalarTower_1, WithVal.toVal_neg, LaurentSeries.exists_powerSeries_of_memIntegers, LaurentSeries.continuous_coe', NumberField.FinitePlace.equivHeightOneSpectrum_symm_apply, NumberField.FinitePlace.norm_def_int, WithVal.algebraMap_left_injective, WithVal.toVal_pow, WithVal.ofVal_sub, NumberField.RingOfIntegers.withValEquiv_apply, WithVal.instIsScalarTower_2, WithVal.toVal_div, WithVal.instFaithfulSMul_1, WithVal.toVal_one, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation, IsDedekindDomain.HeightOneSpectrum.coe_mem_adicCompletionIntegers, WithVal.strictMono_valueGroupEquiv_symm, Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, WithVal.toVal_smul, LaurentSeries.valuation_LaurentSeries_equal_extension, WithVal.ofVal_pow, LaurentSeries.LaurentSeries_coe, LaurentSeries.powerSeries_ext_subring, NumberField.HeightOneSpectrum.instFiniteAdicCompletionRingOfIntegers, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, WithVal.ofVal_smul, WithVal.instFinite_1, WithVal.ofVal_surjective, WithVal.instIsFractionRing, LaurentSeries.powerSeriesRingEquiv_coe_apply, instIsDiscreteValuationRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, WithVal.smul_right_def, WithVal.toVal_eq_zero, WithVal.ofVal_bijective, WithVal.congr_apply, IsDedekindDomain.HeightOneSpectrum.adicValued.uniformContinuousConstSMul, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective, WithVal.map_apply, WithVal.algEquiv_apply, WithVal.ofVal_neg, WithVal.instIsLocalization, Padic.withValUniformEquiv_cast_apply, Padic.coe_withValRingEquiv, NumberField.FinitePlace.norm_eq_one_iff_notMem, WithVal.valueGroupOrderIso₀_symm_restrict, WithVal.toVal_add, LaurentSeries.valuation_compare, Padic.isUniformInducing_cast_withVal, LaurentSeries.tendsto_valuation, WithVal.congr_symm, Valuation.IsEquiv.uniformContinuous_equiv_symm, IsDedekindDomain.HeightOneSpectrum.adicValued_apply', WithVal.equivWithVal_apply, Padic.coe_withValRingEquiv_symm, IsDedekindDomain.HeightOneSpectrum.adicCompletion_valueGroup_eq, LaurentSeries.comparePkg_eq_extension, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletion, WithVal.congr_refl, instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, LaurentSeries.ratfuncAdicComplRingEquiv_apply, WithVal.ofVal_eq_zero, WithVal.le_def, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, WithVal.valuation_equiv_symm, NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbv, NumberField.FinitePlace.norm_embedding', NumberField.FinitePlace.norm_le_one, LaurentSeries.mem_integers_of_powerSeries, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion, WithVal.toVal_injective, WithVal.strictMono_valueGroupEquiv, IsDedekindDomain.HeightOneSpectrum.adicCompletion.mul_nonZeroDivisor_mem_adicCompletionIntegers, WithVal.smul_left_def, WithVal.algebraMap_right_injective, WithVal.equivWithVal_symm_apply, NumberField.FinitePlace.norm_embedding_int, Padic.isDenseInducing_cast_withVal, WithVal.congr_trans, LaurentSeries.uniformContinuous_withVal_equiv, NumberField.FinitePlace.norm_def, Rat.ringOfIntegersWithValEquiv_apply, WithVal.algebraMap_right_apply, IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers, Valuation.IsEquiv.orderRingIso_symm_apply

---

← Back to Index