FinitePlace

📁 Source: Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean

Statistics

Metric	Count
Definitions `FinitePlace`, `embedding`, `equivHeightOneSpectrum`, `instFunLikeReal`, `maximalIdeal`, `mk`, `adicAbv`, `instNormedFieldValuedAdicCompletion`, `instRankOneAdicCompletion`, `adicAbv`, `instNormedFieldValuedAdicCompletion`, `instRankOneAdicCompletion`, `instRankOneWithZeroMultiplicativeIntValuation`, `IsFinitePlace`	14
Theorems `embedding_mul_absNorm`, `equivHeightOneSpectrum_symm_apply`, `add_le`, `coe_apply`, `embedding_apply`, `equivHeightOneSpectrum_symm_apply`, `hasFiniteMulSupport`, `hasFiniteMulSupport_int`, `instMonoidWithZeroHomClassReal`, `instNonarchimedeanHomClassReal`, `instNonnegHomClassReal`, `isFinitePlace`, `maximalIdeal_inj`, `maximalIdeal_injective`, `maximalIdeal_mk`, `mk_apply`, `mk_eq_iff`, `mk_maximalIdeal`, `mulSupport_finite`, `mulSupport_finite_int`, `norm_def`, `norm_def'`, `norm_def_int`, `norm_embedding`, `norm_embedding'`, `norm_embedding_eq`, `norm_embedding_int`, `norm_eq_one_iff_notMem`, `norm_le_one`, `norm_lt_one_iff_mem`, `pos_iff`, `absNorm_ne_zero`, `adicAbv_add_le_max`, `adicAbv_def`, `adicAbv_intCast_le_one`, `adicAbv_natCast_le_one`, `isNonarchimedean_adicAbv`, `one_lt_absNorm`, `one_lt_absNorm_nnreal`, `rankOne_hom'_def`, `toNNReal_valued_eq_adicAbv`, `absNorm_ne_zero`, `adicAbv_add_le_max`, `adicAbv_def`, `adicAbv_intCast_le_one`, `adicAbv_natCast_le_one`, `embedding_mul_absNorm`, `instFiniteAdicCompletionRingOfIntegers`, `isNonarchimedean_adicAbv`, `one_lt_absNorm`, `one_lt_absNorm_nnreal`, `rankOne_hom'_def`, `toNNReal_valued_eq_adicAbv`, `instIsRankOneDiscreteWithZeroMultiplicativeIntAdicCompletionV`, `isFinitePlace_iff`, `instIsDiscreteValuationRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers`, `instIsDiscreteValuationRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation`, `instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers`, `instIsPrincipalIdealRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation`	59
Total	73

NumberField

Definitions

Name	Category	Theorems
`FinitePlace` 📖	CompOp	24 math math: `FinitePlace.hasFiniteMulSupport_int`, `prod_nonarchAbsVal_eq`, `FinitePlace.mk_apply`, `FinitePlace.mulSupport_finite`, `FinitePlace.prod_eq_inv_abs_norm`, `prod_abs_eq_one`, `FinitePlace.prod_eq_inv_abs_norm_int`, `FinitePlace.norm_embedding_eq`, `mulHeight_eq`, `FinitePlace.hasFiniteMulSupport`, `FinitePlace.maximalIdeal_injective`, `FinitePlace.IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply`, `FinitePlace.add_le`, `FinitePlace.instNonnegHomClassReal`, `isFinitePlace_iff`, `sum_nonarchAbsVal_eq`, `logHeight₁_eq`, `FinitePlace.mulSupport_finite_int`, `FinitePlace.coe_apply`, `FinitePlace.equivHeightOneSpectrum_symm_apply`, `FinitePlace.pos_iff`, `FinitePlace.instMonoidWithZeroHomClassReal`, `FinitePlace.instNonarchimedeanHomClassReal`, `mulHeight₁_eq`
`IsFinitePlace` 📖	MathDef	2 math math: `isFinitePlace_iff`, `FinitePlace.isFinitePlace`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsRankOneDiscreteWithZeroMultiplicativeIntAdicCompletionV` 📖	mathematical	—	`Valuation.IsRankOneDiscrete` `WithZero` `Multiplicative` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `Multiplicative.isOrderedMonoid` `Int.instAddCommMonoid` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Int.instIsOrderedAddMonoid` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `UniformSpace.Completion.ring` `WithVal` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `WithVal.instRing` `Valued.toUniformSpace` `WithVal.instValued` `IsTopologicalDivisionRing.toIsTopologicalRing` `WithVal.instField` `UniformSpace.toTopologicalSpace` `Valued.isTopologicalDivisionRing` `Valued.toIsUniformAddGroup` `Valued.v` `Valued.valuedCompletion`	—	`Multiplicative.isOrderedMonoid` `Int.instIsOrderedAddMonoid` `IsTopologicalDivisionRing.toIsTopologicalRing` `Valued.isTopologicalDivisionRing` `Valued.toIsUniformAddGroup` `Valuation.IsRankOneDiscrete.mk'` `Subgroup.isCyclic` `instIsCyclicUnitsWithZero` `isCyclic_multiplicative` `instIsAddCyclicInt` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `Valuation.instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial` `IsDedekindDomain.HeightOneSpectrum.instIsNontrivialWithZeroMultiplicativeIntValuation` `Valuation.IsRankOneDiscrete.generator_zpowers_eq_valueGroup` `Multiplicative.isOrderedCancelMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `Valued.completable` `IsDedekindDomain.HeightOneSpectrum.adicCompletion_valueGroup_eq` `Valuation.IsRankOneDiscrete.generator_lt_one`
`isFinitePlace_iff` 📖	mathematical	—	`IsFinitePlace` `FinitePlace` `AbsoluteValue` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `IsDedekindDomain.HeightOneSpectrum` `RingOfIntegers` `instCommRingRingOfIntegers` `place` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `RingOfIntegers.instIsDedekindDomain` `RingOfIntegers.instAlgebra_1` `RingOfIntegers.instIsFractionRing` `NormedField.toNormedDivisionRing` `HeightOneSpectrum.instNormedFieldValuedAdicCompletion` `RingOfIntegers.instFreeInt` `FinitePlace.embedding`	—	`RingOfIntegers.instIsDedekindDomain` `RingOfIntegers.instIsFractionRing` `RingOfIntegers.instFreeInt` `FinitePlace.isFinitePlace`

NumberField.FinitePlace

Definitions

Name	Category	Theorems
`embedding` 📖	CompOp	20 math math: `NumberField.prod_nonarchAbsVal_eq`, `mk_apply`, `norm_def'`, `embedding_apply`, `norm_embedding_eq`, `norm_embedding`, `norm_lt_one_iff_mem`, `IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm`, `IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply`, `NumberField.isFinitePlace_iff`, `NumberField.sum_nonarchAbsVal_eq`, `NumberField.HeightOneSpectrum.embedding_mul_absNorm`, `coe_apply`, `equivHeightOneSpectrum_symm_apply`, `norm_def_int`, `norm_eq_one_iff_notMem`, `isFinitePlace`, `norm_embedding'`, `norm_le_one`, `norm_embedding_int`
`equivHeightOneSpectrum` 📖	CompOp	2 math math: `IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply`, `equivHeightOneSpectrum_symm_apply`
`instFunLikeReal` 📖	CompOp	20 math math: `hasFiniteMulSupport_int`, `mk_apply`, `mulSupport_finite`, `prod_eq_inv_abs_norm`, `NumberField.prod_abs_eq_one`, `prod_eq_inv_abs_norm_int`, `norm_embedding_eq`, `NumberField.mulHeight_eq`, `hasFiniteMulSupport`, `IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply`, `add_le`, `instNonnegHomClassReal`, `NumberField.logHeight₁_eq`, `mulSupport_finite_int`, `coe_apply`, `equivHeightOneSpectrum_symm_apply`, `pos_iff`, `instMonoidWithZeroHomClassReal`, `instNonarchimedeanHomClassReal`, `NumberField.mulHeight₁_eq`
`maximalIdeal` 📖	CompOp	5 math math: `norm_embedding_eq`, `maximalIdeal_injective`, `mk_maximalIdeal`, `maximalIdeal_inj`, `maximalIdeal_mk`
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_le` 📖	mathematical	—	`Real` `Real.instLE` `DFunLike.coe` `NumberField.FinitePlace` `instFunLikeReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Real.instMax`	—	`NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instIsFractionRing` `NumberField.RingOfIntegers.instFreeInt` `Subtype.prop` `AddMonoid.FG.to_moduleFinite_int` `AddMonoid.fg_of_addGroup_fg` `NumberField.RingOfIntegers.instFG` `NumberField.HeightOneSpectrum.adicAbv_add_le_max`
`coe_apply` 📖	mathematical	—	`DFunLike.coe` `NumberField.FinitePlace` `Real` `instFunLikeReal` `AbsoluteValue` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `IsDedekindDomain.HeightOneSpectrum` `NumberField.RingOfIntegers` `NumberField.instCommRingRingOfIntegers` `NumberField.place` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instAlgebra_1` `NumberField.RingOfIntegers.instIsFractionRing` `NormedField.toNormedDivisionRing` `NumberField.HeightOneSpectrum.instNormedFieldValuedAdicCompletion` `NumberField.RingOfIntegers.instFreeInt` `embedding`	—	—
`embedding_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `UniformSpace.Completion.instField` `WithVal` `WithZero` `Multiplicative` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `WithVal.instField` `Valued.toUniformSpace` `WithVal.instRing` `WithVal.instValued` `Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `RingHom.instFunLike` `embedding` `UniformSpace.Completion.coe'` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `WithVal.equiv`	—	`Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup`
`equivHeightOneSpectrum_symm_apply` 📖	mathematical	—	`DFunLike.coe` `NumberField.FinitePlace` `Real` `instFunLikeReal` `Equiv` `IsDedekindDomain.HeightOneSpectrum` `NumberField.RingOfIntegers` `NumberField.instCommRingRingOfIntegers` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivHeightOneSpectrum` `Norm.norm` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instAlgebra_1` `NumberField.RingOfIntegers.instIsFractionRing` `NormedField.toNorm` `NumberField.HeightOneSpectrum.instNormedFieldValuedAdicCompletion` `AddMonoid.FG.to_moduleFinite_int` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoid.fg_of_addGroup_fg` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `NumberField.RingOfIntegers.instFG` `NumberField.RingOfIntegers.instFreeInt` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `UniformSpace.Completion.instField` `WithVal` `WithZero` `Multiplicative` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `WithVal.instField` `Valued.toUniformSpace` `WithVal.instRing` `WithVal.instValued` `Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `RingHom.instFunLike` `embedding`	—	—
`hasFiniteMulSupport` 📖	mathematical	—	`Function.HasFiniteMulSupport` `NumberField.FinitePlace` `Real` `Real.instOne` `DFunLike.coe` `instFunLikeReal`	—	`IsFractionRing.div_surjective` `NumberField.RingOfIntegers.instIsFractionRing` `map_div₀` `instMonoidWithZeroHomClassReal` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `NumberField.RingOfIntegers.instIsTorsionFree_2` `Function.HasFiniteMulSupport.fun_div` `hasFiniteMulSupport_int`
`hasFiniteMulSupport_int` 📖	mathematical	—	`Function.HasFiniteMulSupport` `NumberField.FinitePlace` `Real` `Real.instOne` `DFunLike.coe` `instFunLikeReal` `NumberField.RingOfIntegers.val`	—	`ne_iff_lt_iff_le` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instIsFractionRing` `AddMonoid.FG.to_moduleFinite_int` `AddMonoid.fg_of_addGroup_fg` `NumberField.RingOfIntegers.instFG` `NumberField.RingOfIntegers.instFreeInt` `Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `norm_le_one` `norm_embedding_eq` `IsScalarTower.right` `Ideal.finite_factors` `Function.Injective.injOn` `maximalIdeal_injective` `Set.Finite.of_finite_image` `Set.Finite.subset` `Set.instReflSubset`
`instMonoidWithZeroHomClassReal` 📖	mathematical	—	`MonoidWithZeroHomClass` `NumberField.FinitePlace` `Real` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `instFunLikeReal`	—	`AbsoluteValue.map_mul` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instIsFractionRing` `NumberField.RingOfIntegers.instFreeInt` `AbsoluteValue.map_one` `Real.instIsDomain` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `AbsoluteValue.map_zero`
`instNonarchimedeanHomClassReal` 📖	mathematical	—	`NonarchimedeanHomClass` `NumberField.FinitePlace` `Real` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Real.linearOrder` `instFunLikeReal`	—	`add_le`
`instNonnegHomClassReal` 📖	mathematical	—	`NonnegHomClass` `NumberField.FinitePlace` `Real` `Real.instZero` `Real.instLE` `instFunLikeReal`	—	`AbsoluteValue.nonneg` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instIsFractionRing` `NumberField.RingOfIntegers.instFreeInt`
`isFinitePlace` 📖	mathematical	—	`NumberField.IsFinitePlace` `AbsoluteValue` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `IsDedekindDomain.HeightOneSpectrum` `NumberField.RingOfIntegers` `NumberField.instCommRingRingOfIntegers` `NumberField.place` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instAlgebra_1` `NumberField.RingOfIntegers.instIsFractionRing` `NormedField.toNormedDivisionRing` `NumberField.HeightOneSpectrum.instNormedFieldValuedAdicCompletion` `NumberField.RingOfIntegers.instFreeInt` `embedding`	—	`Subtype.prop` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instIsFractionRing` `NumberField.RingOfIntegers.instFreeInt`
`maximalIdeal_inj` 📖	mathematical	—	`maximalIdeal`	—	`Equiv.injective`
`maximalIdeal_injective` 📖	mathematical	—	`NumberField.FinitePlace` `IsDedekindDomain.HeightOneSpectrum` `NumberField.RingOfIntegers` `NumberField.instCommRingRingOfIntegers` `maximalIdeal`	—	`Equiv.injective`
`maximalIdeal_mk` 📖	mathematical	—	`maximalIdeal`	—	`mk_eq_iff` `mk_maximalIdeal`
`mk_apply` 📖	mathematical	—	`DFunLike.coe` `NumberField.FinitePlace` `Real` `instFunLikeReal` `Norm.norm` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `NumberField.RingOfIntegers` `NumberField.instCommRingRingOfIntegers` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instAlgebra_1` `NumberField.RingOfIntegers.instIsFractionRing` `NormedField.toNorm` `NumberField.HeightOneSpectrum.instNormedFieldValuedAdicCompletion` `AddMonoid.FG.to_moduleFinite_int` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoid.fg_of_addGroup_fg` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `NumberField.RingOfIntegers.instFG` `NumberField.RingOfIntegers.instFreeInt` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `UniformSpace.Completion.instField` `WithVal` `WithZero` `Multiplicative` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `WithVal.instField` `Valued.toUniformSpace` `WithVal.instRing` `WithVal.instValued` `Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `RingHom.instFunLike` `embedding`	—	—
`mk_eq_iff` 📖	—	—	—	—	`Mathlib.Tactic.Contrapose.contrapose₁` `DFunLike.ne_iff` `IsDedekindDomain.HeightOneSpectrum.ext_iff` `Ideal.IsMaximal.eq_of_le` `IsDedekindDomain.HeightOneSpectrum.isMaximal` `NumberField.RingOfIntegers.instIsDedekindDomain` `Ideal.IsPrime.ne_top'` `IsDedekindDomain.HeightOneSpectrum.isPrime` `Mathlib.Tactic.Push.not_and_eq` `NumberField.RingOfIntegers.instIsFractionRing` `AddMonoid.FG.to_moduleFinite_int` `AddMonoid.fg_of_addGroup_fg` `NumberField.RingOfIntegers.instFG` `NumberField.RingOfIntegers.instFreeInt` `Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `norm_lt_one_iff_mem` `neg_eq_zero` `sub_eq_zero_of_eq` `norm_eq_one_iff_notMem`
`mk_maximalIdeal` 📖	mathematical	—	`maximalIdeal`	—	`NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instIsFractionRing` `NumberField.RingOfIntegers.instFreeInt`
`mulSupport_finite` 📖	mathematical	—	`Function.HasFiniteMulSupport` `NumberField.FinitePlace` `Real` `Real.instOne` `DFunLike.coe` `instFunLikeReal`	—	`hasFiniteMulSupport`
`mulSupport_finite_int` 📖	mathematical	—	`Function.HasFiniteMulSupport` `NumberField.FinitePlace` `Real` `Real.instOne` `DFunLike.coe` `instFunLikeReal` `NumberField.RingOfIntegers.val`	—	`hasFiniteMulSupport_int`
`norm_def` 📖	mathematical	—	`Norm.norm` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `NormedField.toNorm` `NumberField.HeightOneSpectrum.instNormedFieldValuedAdicCompletion` `NNReal.toReal` `DFunLike.coe` `MonoidWithZeroHom` `WithZero` `Multiplicative` `NNReal` `WithZero.instMulZeroOneClass` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `NNReal.instSemiring` `MonoidWithZeroHom.funLike` `WithZeroMulInt.toNNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `Ideal.absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `NumberField.HeightOneSpectrum.absNorm_ne_zero` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `UniformSpace.Completion.ring` `WithVal` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `WithVal.instField` `Valued.toUniformSpace` `WithVal.instValued` `IsTopologicalDivisionRing.toIsTopologicalRing` `UniformSpace.toTopologicalSpace` `Valued.isTopologicalDivisionRing` `Valued.toIsUniformAddGroup` `Valuation.instFunLike` `Valued.v` `Valued.valuedCompletion`	—	`IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `NumberField.HeightOneSpectrum.absNorm_ne_zero` `IsTopologicalDivisionRing.toIsTopologicalRing` `Valued.isTopologicalDivisionRing` `Valued.toIsUniformAddGroup` `Multiplicative.isOrderedCancelMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `Valued.completable` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `Multiplicative.isOrderedMonoid` `Int.instIsOrderedAddMonoid` `NumberField.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicCompletionV` `Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective` `IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective`
`norm_def'` 📖	mathematical	—	`Norm.norm` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `NormedField.toNorm` `NumberField.HeightOneSpectrum.instNormedFieldValuedAdicCompletion` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `UniformSpace.Completion.instField` `WithVal` `WithZero` `Multiplicative` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `WithVal.instField` `Valued.toUniformSpace` `WithVal.instRing` `WithVal.instValued` `Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `RingHom.instFunLike` `embedding` `NNReal.toReal` `MonoidWithZeroHom` `NNReal` `WithZero.instMulZeroOneClass` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `NonAssocSemiring.toMulZeroOneClass` `NNReal.instSemiring` `MonoidWithZeroHom.funLike` `WithZeroMulInt.toNNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `Ideal.absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `NumberField.HeightOneSpectrum.absNorm_ne_zero` `Valuation` `WithZero.instLinearOrderedCommMonoidWithZero` `Multiplicative.commMonoid` `Int.instAddCommMonoid` `Multiplicative.isOrderedCancelMonoid` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `instLatticeInt` `Int.instIsStrictOrderedRing` `Valuation.instFunLike`	—	`norm_embedding'`
`norm_def_int` 📖	mathematical	—	`Norm.norm` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `NormedField.toNorm` `NumberField.HeightOneSpectrum.instNormedFieldValuedAdicCompletion` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `UniformSpace.Completion.instField` `WithVal` `WithZero` `Multiplicative` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `WithVal.instField` `Valued.toUniformSpace` `WithVal.instRing` `WithVal.instValued` `Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `RingHom.instFunLike` `embedding` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `algebraMap` `NNReal.toReal` `MonoidWithZeroHom` `NNReal` `WithZero.instMulZeroOneClass` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `NonAssocSemiring.toMulZeroOneClass` `NNReal.instSemiring` `MonoidWithZeroHom.funLike` `WithZeroMulInt.toNNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Ideal` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `Ideal.absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `NumberField.HeightOneSpectrum.absNorm_ne_zero` `Valuation` `WithZero.instLinearOrderedCommMonoidWithZero` `Multiplicative.commMonoid` `Int.instAddCommMonoid` `Multiplicative.isOrderedCancelMonoid` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `instLatticeInt` `Int.instIsStrictOrderedRing` `CommRing.toRing` `Valuation.instFunLike` `IsDedekindDomain.HeightOneSpectrum.intValuation`	—	`norm_embedding_int`
`norm_embedding` 📖	mathematical	—	`Norm.norm` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `NormedField.toNorm` `NumberField.HeightOneSpectrum.instNormedFieldValuedAdicCompletion` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `UniformSpace.Completion.instField` `WithVal` `WithZero` `Multiplicative` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `WithVal.instField` `Valued.toUniformSpace` `WithVal.instRing` `WithVal.instValued` `Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `RingHom.instFunLike` `embedding` `AbsoluteValue` `Real` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `NumberField.HeightOneSpectrum.adicAbv`	—	`Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `NumberField.HeightOneSpectrum.absNorm_ne_zero` `Multiplicative.isOrderedCancelMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `norm_def` `Valued.valuedCompletion_apply`
`norm_embedding'` 📖	mathematical	—	`Norm.norm` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `NormedField.toNorm` `NumberField.HeightOneSpectrum.instNormedFieldValuedAdicCompletion` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `UniformSpace.Completion.instField` `WithVal` `WithZero` `Multiplicative` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `WithVal.instField` `Valued.toUniformSpace` `WithVal.instRing` `WithVal.instValued` `Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `RingHom.instFunLike` `embedding` `NNReal.toReal` `MonoidWithZeroHom` `NNReal` `WithZero.instMulZeroOneClass` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `NonAssocSemiring.toMulZeroOneClass` `NNReal.instSemiring` `MonoidWithZeroHom.funLike` `WithZeroMulInt.toNNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `Ideal.absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `NumberField.HeightOneSpectrum.absNorm_ne_zero` `Valuation` `WithZero.instLinearOrderedCommMonoidWithZero` `Multiplicative.commMonoid` `Int.instAddCommMonoid` `Multiplicative.isOrderedCancelMonoid` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `instLatticeInt` `Int.instIsStrictOrderedRing` `Valuation.instFunLike`	—	`Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `NumberField.HeightOneSpectrum.absNorm_ne_zero` `Multiplicative.isOrderedCancelMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `norm_embedding` `NumberField.HeightOneSpectrum.adicAbv_def`
`norm_embedding_eq` 📖	mathematical	—	`Norm.norm` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `NumberField.RingOfIntegers` `NumberField.instCommRingRingOfIntegers` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instAlgebra_1` `NumberField.RingOfIntegers.instIsFractionRing` `maximalIdeal` `NormedField.toNorm` `NumberField.HeightOneSpectrum.instNormedFieldValuedAdicCompletion` `AddMonoid.FG.to_moduleFinite_int` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoid.fg_of_addGroup_fg` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `NumberField.RingOfIntegers.instFG` `NumberField.RingOfIntegers.instFreeInt` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `UniformSpace.Completion.instField` `WithVal` `WithZero` `Multiplicative` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `WithVal.instField` `Valued.toUniformSpace` `WithVal.instRing` `WithVal.instValued` `Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `RingHom.instFunLike` `embedding` `NumberField.FinitePlace` `Real` `instFunLikeReal`	—	`NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instIsFractionRing` `AddMonoid.FG.to_moduleFinite_int` `AddMonoid.fg_of_addGroup_fg` `NumberField.RingOfIntegers.instFG` `NumberField.RingOfIntegers.instFreeInt` `Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `mk_maximalIdeal` `mk_apply`
`norm_embedding_int` 📖	mathematical	—	`Norm.norm` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `NormedField.toNorm` `NumberField.HeightOneSpectrum.instNormedFieldValuedAdicCompletion` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `UniformSpace.Completion.instField` `WithVal` `WithZero` `Multiplicative` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `WithVal.instField` `Valued.toUniformSpace` `WithVal.instRing` `WithVal.instValued` `Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `RingHom.instFunLike` `embedding` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `algebraMap` `NNReal.toReal` `MonoidWithZeroHom` `NNReal` `WithZero.instMulZeroOneClass` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `NonAssocSemiring.toMulZeroOneClass` `NNReal.instSemiring` `MonoidWithZeroHom.funLike` `WithZeroMulInt.toNNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Ideal` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `Ideal.absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `NumberField.HeightOneSpectrum.absNorm_ne_zero` `Valuation` `WithZero.instLinearOrderedCommMonoidWithZero` `Multiplicative.commMonoid` `Int.instAddCommMonoid` `Multiplicative.isOrderedCancelMonoid` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `instLatticeInt` `Int.instIsStrictOrderedRing` `CommRing.toRing` `Valuation.instFunLike` `IsDedekindDomain.HeightOneSpectrum.intValuation`	—	`Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `NumberField.HeightOneSpectrum.absNorm_ne_zero` `Multiplicative.isOrderedCancelMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `norm_embedding` `IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap`
`norm_eq_one_iff_notMem` 📖	mathematical	—	`Norm.norm` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `NormedField.toNorm` `NumberField.HeightOneSpectrum.instNormedFieldValuedAdicCompletion` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `UniformSpace.Completion.instField` `WithVal` `WithZero` `Multiplicative` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `WithVal.instField` `Valued.toUniformSpace` `WithVal.instRing` `WithVal.instValued` `Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `RingHom.instFunLike` `embedding` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `algebraMap` `Real` `Real.instOne` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `IsDedekindDomain.HeightOneSpectrum.asIdeal`	—	`Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `norm_embedding` `IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_eq_one_iff` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal`
`norm_le_one` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `NormedField.toNorm` `NumberField.HeightOneSpectrum.instNormedFieldValuedAdicCompletion` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `UniformSpace.Completion.instField` `WithVal` `WithZero` `Multiplicative` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `WithVal.instField` `Valued.toUniformSpace` `WithVal.instRing` `WithVal.instValued` `Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `RingHom.instFunLike` `embedding` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `algebraMap` `Real.instOne`	—	`Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `norm_embedding` `IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_le_one` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal`
`norm_lt_one_iff_mem` 📖	mathematical	—	`Real` `Real.instLT` `Norm.norm` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `NormedField.toNorm` `NumberField.HeightOneSpectrum.instNormedFieldValuedAdicCompletion` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `UniformSpace.Completion.instField` `WithVal` `WithZero` `Multiplicative` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `WithVal.instField` `Valued.toUniformSpace` `WithVal.instRing` `WithVal.instValued` `Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `RingHom.instFunLike` `embedding` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `algebraMap` `Real.instOne` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `IsDedekindDomain.HeightOneSpectrum.asIdeal`	—	`Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `norm_embedding` `IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_lt_one_iff` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal`
`pos_iff` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `DFunLike.coe` `NumberField.FinitePlace` `instFunLikeReal`	—	`AbsoluteValue.pos_iff` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instIsFractionRing` `NumberField.RingOfIntegers.instFreeInt`

NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`embedding_mul_absNorm` 📖	mathematical	—	`Real` `Real.instMul` `Norm.norm` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `NormedField.toNorm` `NumberField.HeightOneSpectrum.instNormedFieldValuedAdicCompletion` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `UniformSpace.Completion.instField` `WithVal` `WithZero` `Multiplicative` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `WithVal.instField` `Valued.toUniformSpace` `WithVal.instRing` `WithVal.instValued` `Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `RingHom.instFunLike` `NumberField.FinitePlace.embedding` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `algebraMap` `Real.instNatCast` `MonoidWithZeroHom` `Ideal` `NonAssocSemiring.toMulZeroOneClass` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `Ideal.absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDedekindDomain.HeightOneSpectrum.maxPowDividing` `Ideal.span` `Set` `Set.instSingletonSet` `Real.instOne`	—	`NumberField.HeightOneSpectrum.embedding_mul_absNorm`
`equivHeightOneSpectrum_symm_apply` 📖	mathematical	—	`DFunLike.coe` `NumberField.FinitePlace` `Real` `NumberField.FinitePlace.instFunLikeReal` `Equiv` `IsDedekindDomain.HeightOneSpectrum` `NumberField.RingOfIntegers` `NumberField.instCommRingRingOfIntegers` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `NumberField.FinitePlace.equivHeightOneSpectrum` `Norm.norm` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instAlgebra_1` `NumberField.RingOfIntegers.instIsFractionRing` `NormedField.toNorm` `NumberField.HeightOneSpectrum.instNormedFieldValuedAdicCompletion` `AddMonoid.FG.to_moduleFinite_int` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoid.fg_of_addGroup_fg` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `NumberField.RingOfIntegers.instFG` `NumberField.RingOfIntegers.instFreeInt` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `UniformSpace.Completion.instField` `WithVal` `WithZero` `Multiplicative` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `WithVal.instField` `Valued.toUniformSpace` `WithVal.instRing` `WithVal.instValued` `Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `RingHom.instFunLike` `NumberField.FinitePlace.embedding`	—	`NumberField.FinitePlace.equivHeightOneSpectrum_symm_apply`

NumberField.HeightOneSpectrum

Definitions

Name	Category	Theorems
`adicAbv` 📖	CompOp	13 math math: `NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_natCast_le_one`, `NumberField.RingOfIntegers.HeightOneSpectrum.isNonarchimedean_adicAbv`, `NumberField.toNNReal_valued_eq_adicAbv`, `adicAbv_natCast_le_one`, `NumberField.FinitePlace.norm_embedding`, `adicAbv_def`, `NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_intCast_le_one`, `isNonarchimedean_adicAbv`, `adicAbv_add_le_max`, `adicAbv_intCast_le_one`, `NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def`, `NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_add_le_max`, `toNNReal_valued_eq_adicAbv`
`instNormedFieldValuedAdicCompletion` 📖	CompOp	21 math math: `NumberField.prod_nonarchAbsVal_eq`, `NumberField.FinitePlace.mk_apply`, `NumberField.FinitePlace.norm_def'`, `NumberField.FinitePlace.norm_embedding_eq`, `NumberField.FinitePlace.norm_embedding`, `NumberField.FinitePlace.norm_lt_one_iff_mem`, `NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm`, `NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply`, `NumberField.isFinitePlace_iff`, `NumberField.sum_nonarchAbsVal_eq`, `embedding_mul_absNorm`, `NumberField.FinitePlace.coe_apply`, `NumberField.FinitePlace.equivHeightOneSpectrum_symm_apply`, `NumberField.FinitePlace.norm_def_int`, `instFiniteAdicCompletionRingOfIntegers`, `NumberField.FinitePlace.norm_eq_one_iff_notMem`, `NumberField.FinitePlace.isFinitePlace`, `NumberField.FinitePlace.norm_embedding'`, `NumberField.FinitePlace.norm_le_one`, `NumberField.FinitePlace.norm_embedding_int`, `NumberField.FinitePlace.norm_def`
`instRankOneAdicCompletion` 📖	CompOp	2 math math: `rankOne_hom'_def`, `NumberField.rankOne_hom'_def`
`instRankOneWithZeroMultiplicativeIntValuation` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`absNorm_ne_zero` 📖	—	—	—	—	`ne_zero_of_lt` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `one_lt_absNorm_nnreal`
`adicAbv_add_le_max` 📖	mathematical	—	`Real` `Real.instLE` `DFunLike.coe` `AbsoluteValue` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `adicAbv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Real.instMax`	—	`isNonarchimedean_adicAbv`
`adicAbv_def` 📖	mathematical	—	`DFunLike.coe` `AbsoluteValue` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `adicAbv` `NNReal.toReal` `MonoidWithZeroHom` `WithZero` `Multiplicative` `NNReal` `WithZero.instMulZeroOneClass` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `NNReal.instSemiring` `MonoidWithZeroHom.funLike` `WithZeroMulInt.toNNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `Ideal.absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `absNorm_ne_zero` `Valuation` `WithZero.instLinearOrderedCommMonoidWithZero` `Multiplicative.commMonoid` `Int.instAddCommMonoid` `Multiplicative.linearOrder` `Int.instLinearOrder` `Multiplicative.isOrderedCancelMonoid` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `instLatticeInt` `Int.instIsStrictOrderedRing` `DivisionRing.toRing` `Field.toDivisionRing` `Valuation.instFunLike` `IsDedekindDomain.HeightOneSpectrum.valuation`	—	—
`adicAbv_intCast_le_one` 📖	mathematical	—	`Real` `Real.instLE` `DFunLike.coe` `AbsoluteValue` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `adicAbv` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Real.instOne`	—	`IsNonarchimedean.apply_intCast_le_one_of_isNonarchimedean` `Real.instIsStrictOrderedRing` `AbsoluteValue.addGroupSeminormClass` `Real.instIsOrderedRing` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `AbsoluteValue.monoidWithZeroHomClass` `Real.instIsDomain` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `isNonarchimedean_adicAbv`
`adicAbv_natCast_le_one` 📖	mathematical	—	`Real` `Real.instLE` `DFunLike.coe` `AbsoluteValue` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `adicAbv` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Real.instOne`	—	`IsNonarchimedean.apply_natCast_le_one_of_isNonarchimedean` `AbsoluteValue.zeroHomClass` `AbsoluteValue.nonnegHomClass` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `AbsoluteValue.monoidWithZeroHomClass` `Real.instIsDomain` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `isNonarchimedean_adicAbv`
`embedding_mul_absNorm` 📖	mathematical	—	`Real` `Real.instMul` `Norm.norm` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `NormedField.toNorm` `instNormedFieldValuedAdicCompletion` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `UniformSpace.Completion.instField` `WithVal` `WithZero` `Multiplicative` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `WithVal.instField` `Valued.toUniformSpace` `WithVal.instRing` `WithVal.instValued` `Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `RingHom.instFunLike` `NumberField.FinitePlace.embedding` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `algebraMap` `Real.instNatCast` `MonoidWithZeroHom` `Ideal` `NonAssocSemiring.toMulZeroOneClass` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `Ideal.absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDedekindDomain.HeightOneSpectrum.maxPowDividing` `Ideal.span` `Set` `Set.instSingletonSet` `Real.instOne`	—	`Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `Ideal.uniqueFactorizationMonoid` `IsDedekindDomain.HeightOneSpectrum.maxPowDividing.eq_1` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `Nat.cast_pow` `NumberField.FinitePlace.norm_embedding` `absNorm_ne_zero` `Multiplicative.isOrderedCancelMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `adicAbv_def` `Valuation.ne_zero_iff` `WithZero.instNontrivial` `Iff.not` `FaithfulSMul.algebraMap_eq_zero_iff` `IsFractionRing.instFaithfulSMul` `WithZeroMulInt.toNNReal_neg_apply` `NNReal.coe_natCast` `zpow_natCast` `zpow_add₀` `Nat.cast_zero` `IsStrictOrderedRing.toCharZero` `RCLike.charZero_rclike` `LT.lt.ne'` `LT.lt.trans` `zero_lt_one` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `NeZero.charZero_one` `one_lt_absNorm_nnreal` `Nat.cast_one` `zpow_eq_one_iff_right₀` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.instZeroLEOneClass` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `WithZero.unzero.congr_simp` `IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap` `IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg` `Associates.count.congr_simp` `neg_add_cancel`
`instFiniteAdicCompletionRingOfIntegers` 📖	mathematical	—	`Module.Finite` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `NumberField.RingOfIntegers` `NumberField.instCommRingRingOfIntegers` `NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instAlgebra_1` `NumberField.RingOfIntegers.instIsFractionRing` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `UniformSpace.Completion.instField` `WithVal` `WithZero` `Multiplicative` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `WithVal.instField` `Valued.toUniformSpace` `WithVal.instRing` `WithVal.instValued` `Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `UniformSpace.Completion.uniformSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `instNormedFieldValuedAdicCompletion` `AddMonoid.FG.to_moduleFinite_int` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoid.fg_of_addGroup_fg` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `NumberField.RingOfIntegers.instFG` `NumberField.RingOfIntegers.instFreeInt` `Algebra.toModule` `Semifield.toCommSemiring`	—	`NumberField.RingOfIntegers.instIsDedekindDomain` `NumberField.RingOfIntegers.instIsFractionRing` `Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `AddMonoid.FG.to_moduleFinite_int` `AddMonoid.fg_of_addGroup_fg` `NumberField.RingOfIntegers.instFG` `NumberField.RingOfIntegers.instFreeInt` `IsDedekindDomain.HeightOneSpectrum.adicValued.uniformContinuousConstSMul` `Algebra.to_smulCommClass` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `IsScalarTower.left` `UniformSpace.Completion.instIsScalarTower` `WithVal.instIsScalarTower_1` `mul_comm` `Dense.mono` `IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `one_mul` `Module.Finite.of_surjective` `RingHomSurjective.ids` `Module.Finite.base_change` `NumberField.instFiniteDimensional` `Set.range_eq_univ` `LinearMap.coe_range` `IsClosed.closure_eq` `Submodule.closed_of_finiteDimensional` `UniformSpace.Completion.completeSpace` `NonarchimedeanAddGroup.toIsTopologicalAddGroup` `IsUltrametricDist.nonarchimedeanAddGroup` `Valued.instIsUltrametricDist` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `LinearMap.finiteDimensional_range` `DenseRange.closure_range`
`isNonarchimedean_adicAbv` 📖	mathematical	—	`IsNonarchimedean` `Real` `Real.linearOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DFunLike.coe` `AbsoluteValue` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `adicAbv`	—	`IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_adicAbv` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `one_lt_absNorm_nnreal`
`one_lt_absNorm` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `Ideal.absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDedekindDomain.HeightOneSpectrum.asIdeal`	—	`IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `Ideal.IsPrime.ne_top` `IsDedekindDomain.HeightOneSpectrum.isPrime` `Ideal.absNorm_eq_one_iff` `Ideal.absNorm_ne_zero_iff` `Ideal.finiteQuotientOfFreeOfNeBot` `IsDedekindDomain.HeightOneSpectrum.ne_bot`
`one_lt_absNorm_nnreal` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `NNReal.instPartialOrder` `NNReal.instOne` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `NNReal.instSemiring` `DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `Ideal.absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDedekindDomain.HeightOneSpectrum.asIdeal`	—	`IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `Nat.cast_one` `NNReal.addLeftMono` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `IsStrictOrderedRing.toCharZero` `one_lt_absNorm`
`rankOne_hom'_def` 📖	mathematical	—	`Valuation.RankLeOne.hom'` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `WithZero` `Multiplicative` `UniformSpace.Completion.ring` `WithVal` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `WithVal.instRing` `Valued.toUniformSpace` `WithVal.instValued` `IsTopologicalDivisionRing.toIsTopologicalRing` `WithVal.instField` `UniformSpace.toTopologicalSpace` `Valued.isTopologicalDivisionRing` `Valued.toIsUniformAddGroup` `Multiplicative.isOrderedMonoid` `Int.instAddCommMonoid` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Int.instIsOrderedAddMonoid` `Valued.v` `Valued.valuedCompletion` `Valuation.RankOne.toRankLeOne` `instRankOneAdicCompletion` `MonoidWithZeroHom.comp` `MonoidWithZeroHom.ValueGroup₀` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `Valuation.instFunLike` `Semiring.toMonoidWithZero` `Ring.toSemiring` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `NNReal` `WithZero.instMulZeroOneClass` `Units` `MonoidWithZero.toMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidWithZeroHom.valueGroup` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `NNReal.instSemiring` `WithZeroMulInt.toNNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `Ideal.absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `absNorm_ne_zero` `MulEquiv.toMonoidWithZeroHom` `Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt` `UniformSpace.Completion.commRing` `WithVal.instCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toRing` `NumberField.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicCompletionV`	—	`Multiplicative.isOrderedMonoid` `Int.instIsOrderedAddMonoid` `IsTopologicalDivisionRing.toIsTopologicalRing` `Valued.isTopologicalDivisionRing` `Valued.toIsUniformAddGroup` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass`
`toNNReal_valued_eq_adicAbv` 📖	mathematical	—	`NNReal.toReal` `DFunLike.coe` `MonoidWithZeroHom` `WithZero` `Multiplicative` `NNReal` `WithZero.instMulZeroOneClass` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `NNReal.instSemiring` `MonoidWithZeroHom.funLike` `WithZeroMulInt.toNNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `Ideal.absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `absNorm_ne_zero` `Valuation` `WithVal` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `Multiplicative.isOrderedMonoid` `Int.instAddCommMonoid` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Int.instIsOrderedAddMonoid` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `WithVal.instRing` `Valuation.instFunLike` `Valued.v` `WithVal.instValued` `AbsoluteValue` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `adicAbv` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `WithVal.equiv`	—	`Multiplicative.isOrderedMonoid` `Int.instIsOrderedAddMonoid` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `absNorm_ne_zero`

NumberField.HeightOneSpectrum.NumberField

Definitions

Name	Category	Theorems
`instNormedFieldValuedAdicCompletion` 📖	CompOp	—
`instRankOneAdicCompletion` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`rankOne_hom'_def` 📖	mathematical	—	`Valuation.RankLeOne.hom'` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `WithZero` `Multiplicative` `UniformSpace.Completion.ring` `WithVal` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `WithVal.instRing` `Valued.toUniformSpace` `WithVal.instValued` `IsTopologicalDivisionRing.toIsTopologicalRing` `WithVal.instField` `UniformSpace.toTopologicalSpace` `Valued.isTopologicalDivisionRing` `Valued.toIsUniformAddGroup` `Multiplicative.isOrderedMonoid` `Int.instAddCommMonoid` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Int.instIsOrderedAddMonoid` `Valued.v` `Valued.valuedCompletion` `Valuation.RankOne.toRankLeOne` `NumberField.HeightOneSpectrum.instRankOneAdicCompletion` `MonoidWithZeroHom.comp` `MonoidWithZeroHom.ValueGroup₀` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `Valuation.instFunLike` `Semiring.toMonoidWithZero` `Ring.toSemiring` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `NNReal` `WithZero.instMulZeroOneClass` `Units` `MonoidWithZero.toMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidWithZeroHom.valueGroup` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `NNReal.instSemiring` `WithZeroMulInt.toNNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `Ideal.absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `NumberField.HeightOneSpectrum.absNorm_ne_zero` `MulEquiv.toMonoidWithZeroHom` `Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt` `UniformSpace.Completion.commRing` `WithVal.instCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommRing.toRing` `NumberField.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicCompletionV`	—	`NumberField.HeightOneSpectrum.rankOne_hom'_def`
`toNNReal_valued_eq_adicAbv` 📖	mathematical	—	`NNReal.toReal` `DFunLike.coe` `MonoidWithZeroHom` `WithZero` `Multiplicative` `NNReal` `WithZero.instMulZeroOneClass` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `NNReal.instSemiring` `MonoidWithZeroHom.funLike` `WithZeroMulInt.toNNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `Ideal.absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `NumberField.HeightOneSpectrum.absNorm_ne_zero` `Valuation` `WithVal` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `Multiplicative.isOrderedMonoid` `Int.instAddCommMonoid` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Int.instIsOrderedAddMonoid` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `WithVal.instRing` `Valuation.instFunLike` `Valued.v` `WithVal.instValued` `AbsoluteValue` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `NumberField.HeightOneSpectrum.adicAbv` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `WithVal.equiv`	—	`NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbv`

NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum

Definitions

Name	Category	Theorems
`adicAbv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`absNorm_ne_zero` 📖	—	—	—	—	`NumberField.HeightOneSpectrum.absNorm_ne_zero`
`adicAbv_add_le_max` 📖	mathematical	—	`Real` `Real.instLE` `DFunLike.coe` `AbsoluteValue` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `NumberField.HeightOneSpectrum.adicAbv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Real.instMax`	—	`NumberField.HeightOneSpectrum.adicAbv_add_le_max`
`adicAbv_def` 📖	mathematical	—	`DFunLike.coe` `AbsoluteValue` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `NumberField.HeightOneSpectrum.adicAbv` `NNReal.toReal` `MonoidWithZeroHom` `WithZero` `Multiplicative` `NNReal` `WithZero.instMulZeroOneClass` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `NNReal.instSemiring` `MonoidWithZeroHom.funLike` `WithZeroMulInt.toNNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `Ideal.absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `NumberField.HeightOneSpectrum.absNorm_ne_zero` `Valuation` `WithZero.instLinearOrderedCommMonoidWithZero` `Multiplicative.commMonoid` `Int.instAddCommMonoid` `Multiplicative.linearOrder` `Int.instLinearOrder` `Multiplicative.isOrderedCancelMonoid` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `instLatticeInt` `Int.instIsStrictOrderedRing` `DivisionRing.toRing` `Field.toDivisionRing` `Valuation.instFunLike` `IsDedekindDomain.HeightOneSpectrum.valuation`	—	`NumberField.HeightOneSpectrum.adicAbv_def`
`adicAbv_intCast_le_one` 📖	mathematical	—	`Real` `Real.instLE` `DFunLike.coe` `AbsoluteValue` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `NumberField.HeightOneSpectrum.adicAbv` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Real.instOne`	—	`NumberField.HeightOneSpectrum.adicAbv_intCast_le_one`
`adicAbv_natCast_le_one` 📖	mathematical	—	`Real` `Real.instLE` `DFunLike.coe` `AbsoluteValue` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `NumberField.HeightOneSpectrum.adicAbv` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Real.instOne`	—	`NumberField.HeightOneSpectrum.adicAbv_natCast_le_one`
`isNonarchimedean_adicAbv` 📖	mathematical	—	`IsNonarchimedean` `Real` `Real.linearOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DFunLike.coe` `AbsoluteValue` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `NumberField.HeightOneSpectrum.adicAbv`	—	`NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv`
`one_lt_absNorm` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `Ideal.absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDedekindDomain.HeightOneSpectrum.asIdeal`	—	`NumberField.HeightOneSpectrum.one_lt_absNorm`
`one_lt_absNorm_nnreal` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `NNReal.instPartialOrder` `NNReal.instOne` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `NNReal.instSemiring` `DFunLike.coe` `MonoidWithZeroHom` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toMulZeroOneClass` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `Ideal.absNorm` `IsDomain.toNontrivial` `IsDedekindDomain.toIsDomain` `IsDedekindDomain.HeightOneSpectrum.asIdeal`	—	`NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsDiscreteValuationRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers` 📖	mathematical	—	`IsDiscreteValuationRing` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `ValuationSubring` `UniformSpace.Completion.instField` `WithVal` `WithZero` `Multiplicative` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `WithVal.instField` `Valued.toUniformSpace` `WithVal.instRing` `WithVal.instValued` `Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `SetLike.instMembership` `ValuationSubring.instSetLike` `IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers` `ValuationSubring.instCommRingSubtypeMem` `ValuationSubring.instIsDomainSubtypeMem`	—	`Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `ValuationSubring.instIsDomainSubtypeMem` `instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers` `ValuationSubring.isLocalRing` `Multiplicative.isOrderedCancelMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer` `Multiplicative.isOrderedMonoid` `Int.instIsOrderedAddMonoid` `IsTopologicalDivisionRing.toIsTopologicalRing` `Valued.valuedCompletion_apply` `Int.instAddLeftMono` `Int.instZeroLEOneClass` `MonoidWithZeroHom.map_eq_zero_iff` `WithZero.instNontrivial`
`instIsDiscreteValuationRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation` 📖	mathematical	—	`IsDiscreteValuationRing` `Subring` `Ring.toNonAssocRing` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subring.instSetLike` `Valuation.integer` `WithZero` `Multiplicative` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `Multiplicative.isOrderedMonoid` `Int.instAddCommMonoid` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Int.instIsOrderedAddMonoid` `IsDedekindDomain.HeightOneSpectrum.valuation` `Subring.toCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Subring.instIsDomainSubtypeMem` `instIsDomain` `Field.toSemifield`	—	`Valuation.valuationSubring_isDiscreteValuationRing` `Multiplicative.isOrderedMonoid` `Int.instIsOrderedAddMonoid` `Valuation.IsRankOneDiscrete.instIsCyclicSubtypeUnitsMemSubgroupValueGroup` `Valuation.IsRankOneDiscrete.mk'` `Subgroup.isCyclic` `instIsCyclicUnitsWithZero` `isCyclic_multiplicative` `instIsAddCyclicInt` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `Valuation.instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial` `IsDedekindDomain.HeightOneSpectrum.instIsNontrivialWithZeroMultiplicativeIntValuation`
`instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers` 📖	mathematical	—	`IsPrincipalIdealRing` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `ValuationSubring` `UniformSpace.Completion.instField` `WithVal` `WithZero` `Multiplicative` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `WithVal.instField` `Valued.toUniformSpace` `WithVal.instRing` `WithVal.instValued` `Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `SetLike.instMembership` `ValuationSubring.instSetLike` `IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `UniformSpace.Completion.commRing` `WithVal.instCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsTopologicalDivisionRing.toIsTopologicalRing` `UniformSpace.toTopologicalSpace` `ValuationSubring.instSubringClass`	—	`Valued.isTopologicalDivisionRing` `Valued.completable` `Valued.toIsUniformAddGroup` `SubringClass.toSubsemiringClass` `IsTopologicalDivisionRing.toIsTopologicalRing` `ValuationSubring.instSubringClass` `Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered` `SubmonoidClass.instMulArchimedean` `WithZero.instMulArchimedean` `Multiplicative.instMulArchimedean` `instArchimedeanInt` `MonoidWithZeroHomClass.toMonoidHomClass` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `Valuation.valuationSubring.integers` `WithZero.denselyOrdered_set_iff_subsingleton` `MonoidWithZeroHom.range_nontrivial` `WithZero.instNontrivial`
`instIsPrincipalIdealRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation` 📖	mathematical	—	`IsPrincipalIdealRing` `Subring` `Ring.toNonAssocRing` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subring.instSetLike` `Valuation.integer` `WithZero` `Multiplicative` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `Multiplicative.isOrderedMonoid` `Int.instAddCommMonoid` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Int.instIsOrderedAddMonoid` `IsDedekindDomain.HeightOneSpectrum.valuation` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Subring.instSubringClass`	—	`Multiplicative.isOrderedMonoid` `Int.instIsOrderedAddMonoid` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered` `SubmonoidClass.instMulArchimedean` `WithZero.instMulArchimedean` `Multiplicative.instMulArchimedean` `instArchimedeanInt` `MonoidWithZeroHomClass.toMonoidHomClass` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `Valuation.integer.integers` `WithZero.denselyOrdered_set_iff_subsingleton` `MonoidWithZeroHom.range_nontrivial` `Multiplicative.isOrderedCancelMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `WithZero.instNontrivial`

---

← Back to Index