FinitePlaces

📁 Source: Mathlib/NumberTheory/NumberField/FinitePlaces.lean

Statistics

Metric	Count
Definitions FinitePlace, embedding, equivHeightOneSpectrum, instFunLikeReal, maximalIdeal, mk, IsFinitePlace, adicAbv, instNormedFieldValuedAdicCompletion, instRankOneValuedAdicCompletion, instRankOneWithZeroMultiplicativeIntValuationRingOfIntegers	11
Theorems embedding_mul_absNorm, equivHeightOneSpectrum_symm_apply, add_le, coe_apply, embedding_apply, 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_eq, 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, isFinitePlace_iff, toNNReal_valued_eq_adicAbv, instIsDiscreteValuationRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, instIsDiscreteValuationRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation, instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, instIsPrincipalIdealRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation	39
Total	50

IsDedekindDomain.HeightOneSpectrum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
embedding_mul_absNorm 📖	mathematical	—	Real Real.instMul Norm.norm adicCompletion NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Field.toSemifield NumberField.RingOfIntegers.instIsFractionRing NormedField.toNorm NumberField.instNormedFieldValuedAdicCompletion DFunLike.coe RingHom WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid valuation Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring WithVal.instField UniformSpace.Completion.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup RingHom.instFunLike NumberField.FinitePlace.embedding NumberField.RingOfIntegers.val Real.instNatCast MonoidWithZeroHom Ideal CommSemiring.toSemiring CommRing.toCommSemiring NonAssocSemiring.toMulZeroOneClass IdemSemiring.toSemiring Submodule.idemSemiring Nat.instMulZeroOneClass MonoidWithZeroHom.funLike Ideal.absNorm NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instFreeInt maxPowDividing Ideal.span Set Set.instSingletonSet Real.instOne	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instIsFractionRing Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instFreeInt Ideal.uniqueFactorizationMonoid maxPowDividing.eq_1 map_pow MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass Nat.cast_pow NumberField.FinitePlace.norm_def NumberField.RingOfIntegers.HeightOneSpectrum.absNorm_ne_zero Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def Valuation.ne_zero_iff WithZero.instNontrivial NumberField.RingOfIntegers.coe_ne_zero_iff WithZeroMulInt.toNNReal_neg_apply NNReal.coe_natCast zpow_natCast zpow_add₀ Nat.cast_zero IsStrictOrderedRing.toCharZero NNReal.instIsStrictOrderedRing RCLike.charZero_rclike LT.lt.ne' LT.lt.trans zero_lt_one LinearOrderedCommMonoidWithZero.toZeroLeOneClass NeZero.charZero_one NumberField.RingOfIntegers.HeightOneSpectrum.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 valuation_of_algebraMap intValuation_if_neg Associates.count.congr_simp neg_add_cancel
equivHeightOneSpectrum_symm_apply 📖	mathematical	—	DFunLike.coe NumberField.FinitePlace Real NumberField.FinitePlace.instFunLikeReal Equiv IsDedekindDomain.HeightOneSpectrum NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing EquivLike.toFunLike Equiv.instEquivLike Equiv.symm NumberField.FinitePlace.equivHeightOneSpectrum Norm.norm adicCompletion NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Field.toSemifield NumberField.RingOfIntegers.instIsFractionRing NormedField.toNorm NumberField.instNormedFieldValuedAdicCompletion RingHom WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid valuation Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring WithVal.instField UniformSpace.Completion.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup RingHom.instFunLike NumberField.FinitePlace.embedding	—	—

NumberField

Definitions

Name	Category	Theorems
FinitePlace 📖	CompOp	18 math math: 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, IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply, FinitePlace.maximalIdeal_injective, FinitePlace.add_le, FinitePlace.instNonnegHomClassReal, FinitePlace.mulSupport_finite_int, FinitePlace.coe_apply, FinitePlace.pos_iff, FinitePlace.instMonoidWithZeroHomClassReal, FinitePlace.instNonarchimedeanHomClassReal, mulHeight₁_eq
IsFinitePlace 📖	MathDef	2 math math: isFinitePlace_iff, FinitePlace.isFinitePlace
instNormedFieldValuedAdicCompletion 📖	CompOp	14 math math: prod_nonarchAbsVal_eq, FinitePlace.mk_apply, FinitePlace.norm_def', FinitePlace.norm_embedding_eq, IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply, FinitePlace.norm_lt_one_iff_mem, isFinitePlace_iff, FinitePlace.coe_apply, FinitePlace.norm_def_int, FinitePlace.norm_eq_one_iff_notMem, FinitePlace.isFinitePlace, IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, FinitePlace.norm_le_one, FinitePlace.norm_def
instRankOneValuedAdicCompletion 📖	CompOp	—
instRankOneWithZeroMultiplicativeIntValuationRingOfIntegers 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isFinitePlace_iff 📖	mathematical	—	IsFinitePlace AbsoluteValue Real DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Real.semiring Real.partialOrder IsDedekindDomain.HeightOneSpectrum RingOfIntegers RingOfIntegers.instCommRing WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing IsDedekindDomain.HeightOneSpectrum.valuation RingOfIntegers.instIsDedekindDomain RingOfIntegers.instAlgebra_1 Algebra.id Semifield.toCommSemiring RingOfIntegers.instIsFractionRing WithVal.instField place IsDedekindDomain.HeightOneSpectrum.adicCompletion NormedField.toNormedDivisionRing instNormedFieldValuedAdicCompletion FinitePlace.embedding	—	RingOfIntegers.instIsDedekindDomain RingOfIntegers.instIsFractionRing FinitePlace.isFinitePlace
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 instSemiringNNReal MonoidWithZeroHom.funLike WithZeroMulInt.toNNReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Ideal RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring RingOfIntegers.instCommRing IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass Ideal.absNorm RingOfIntegers.instNontrivial RingOfIntegers.instIsDedekindDomain RingOfIntegers.instFreeInt IsDedekindDomain.HeightOneSpectrum.asIdeal RingOfIntegers.HeightOneSpectrum.absNorm_ne_zero Valuation WithVal WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid DivisionRing.toRing Field.toDivisionRing IsDedekindDomain.HeightOneSpectrum.valuation RingOfIntegers.instAlgebra_1 Semifield.toCommSemiring Field.toSemifield RingOfIntegers.instIsFractionRing LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithVal.instRing Valuation.instFunLike Valued.v WithVal.instValued AbsoluteValue Real DivisionSemiring.toSemiring Semifield.toDivisionSemiring Real.semiring Real.partialOrder AbsoluteValue.funLike RingOfIntegers.HeightOneSpectrum.adicAbv	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid RingOfIntegers.instIsDedekindDomain RingOfIntegers.instIsFractionRing RingOfIntegers.instNontrivial RingOfIntegers.instFreeInt RingOfIntegers.HeightOneSpectrum.absNorm_ne_zero

NumberField.FinitePlace

Definitions

Name	Category	Theorems
embedding 📖	CompOp	15 math math: NumberField.prod_nonarchAbsVal_eq, mk_apply, norm_def', embedding_apply, norm_embedding_eq, IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply, norm_lt_one_iff_mem, NumberField.isFinitePlace_iff, coe_apply, norm_def_int, norm_eq_one_iff_notMem, isFinitePlace, IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, norm_le_one, norm_def
equivHeightOneSpectrum 📖	CompOp	1 math math: IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply
instFunLikeReal 📖	CompOp	16 math math: 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, IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply, add_le, instNonnegHomClassReal, mulSupport_finite_int, coe_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 Subtype.prop NumberField.RingOfIntegers.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.RingOfIntegers.instCommRing WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing IsDedekindDomain.HeightOneSpectrum.valuation NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instAlgebra_1 Algebra.id Semifield.toCommSemiring NumberField.RingOfIntegers.instIsFractionRing WithVal.instField NumberField.place IsDedekindDomain.HeightOneSpectrum.adicCompletion NormedField.toNormedDivisionRing NumberField.instNormedFieldValuedAdicCompletion embedding	—	—
embedding_apply 📖	mathematical	—	DFunLike.coe RingHom WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid DivisionRing.toRing Field.toDivisionRing IsDedekindDomain.HeightOneSpectrum.valuation NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instAlgebra_1 Algebra.id Semifield.toCommSemiring Field.toSemifield NumberField.RingOfIntegers.instIsFractionRing IsDedekindDomain.HeightOneSpectrum.adicCompletion Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring WithVal.instField UniformSpace.Completion.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup RingHom.instFunLike embedding UniformSpace.Completion.coe'	—	NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instIsFractionRing Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup
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 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
isFinitePlace 📖	mathematical	—	NumberField.IsFinitePlace AbsoluteValue Real DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Real.semiring Real.partialOrder IsDedekindDomain.HeightOneSpectrum NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing IsDedekindDomain.HeightOneSpectrum.valuation NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instAlgebra_1 Algebra.id Semifield.toCommSemiring NumberField.RingOfIntegers.instIsFractionRing WithVal.instField NumberField.place IsDedekindDomain.HeightOneSpectrum.adicCompletion NormedField.toNormedDivisionRing NumberField.instNormedFieldValuedAdicCompletion embedding	—	Subtype.prop NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instIsFractionRing
maximalIdeal_inj 📖	mathematical	—	maximalIdeal	—	Equiv.injective
maximalIdeal_injective 📖	mathematical	—	NumberField.FinitePlace IsDedekindDomain.HeightOneSpectrum NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing 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.RingOfIntegers.instCommRing NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Field.toSemifield NumberField.RingOfIntegers.instIsFractionRing NormedField.toNorm NumberField.instNormedFieldValuedAdicCompletion RingHom WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid IsDedekindDomain.HeightOneSpectrum.valuation Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring WithVal.instField UniformSpace.Completion.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 Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid 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
mulSupport_finite 📖	mathematical	—	Set.Finite NumberField.FinitePlace Function.mulSupport Real Real.instOne DFunLike.coe instFunLikeReal	—	IsFractionRing.div_surjective NumberField.RingOfIntegers.instIsFractionRing map_div₀ instMonoidWithZeroHomClassReal Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero NumberField.RingOfIntegers.instIsDomain IsLocalRing.toNontrivial Field.instIsLocalRing NumberField.RingOfIntegers.instIsTorsionFree_2 Set.Finite.subset Set.Finite.union mulSupport_finite_int Mathlib.Tactic.Contrapose.contrapose₂ div_self NeZero.charZero_one RCLike.charZero_rclike
mulSupport_finite_int 📖	mathematical	—	Set.Finite NumberField.FinitePlace Function.mulSupport Real Real.instOne DFunLike.coe instFunLikeReal NumberField.RingOfIntegers.val	—	ne_iff_lt_iff_le NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instIsFractionRing Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup norm_le_one norm_embedding_eq IsScalarTower.right NumberField.RingOfIntegers.instIsDedekindDomainWithVal Ideal.finite_factors Function.Injective.injOn maximalIdeal_injective Set.Finite.of_finite_image Set.Finite.subset Set.instReflSubset
norm_def 📖	mathematical	—	Norm.norm IsDedekindDomain.HeightOneSpectrum.adicCompletion NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Field.toSemifield NumberField.RingOfIntegers.instIsFractionRing NormedField.toNorm NumberField.instNormedFieldValuedAdicCompletion DFunLike.coe RingHom WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid IsDedekindDomain.HeightOneSpectrum.valuation Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring WithVal.instField UniformSpace.Completion.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.RingOfIntegers.HeightOneSpectrum.adicAbv	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instIsFractionRing Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instFreeInt NumberField.RingOfIntegers.HeightOneSpectrum.absNorm_ne_zero Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Valued.valuedCompletion_apply
norm_def' 📖	mathematical	—	Norm.norm IsDedekindDomain.HeightOneSpectrum.adicCompletion NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Field.toSemifield NumberField.RingOfIntegers.instIsFractionRing NormedField.toNorm NumberField.instNormedFieldValuedAdicCompletion DFunLike.coe RingHom WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid IsDedekindDomain.HeightOneSpectrum.valuation Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring WithVal.instField UniformSpace.Completion.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 instSemiringNNReal MonoidWithZeroHom.funLike WithZeroMulInt.toNNReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Ideal CommSemiring.toSemiring CommRing.toCommSemiring IdemSemiring.toSemiring Submodule.idemSemiring Nat.instMulZeroOneClass Ideal.absNorm NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instFreeInt IsDedekindDomain.HeightOneSpectrum.asIdeal NumberField.RingOfIntegers.HeightOneSpectrum.absNorm_ne_zero Valuation WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing Valuation.instFunLike	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instIsFractionRing Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instFreeInt NumberField.RingOfIntegers.HeightOneSpectrum.absNorm_ne_zero Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing norm_def NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def
norm_def_int 📖	mathematical	—	Norm.norm IsDedekindDomain.HeightOneSpectrum.adicCompletion NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Field.toSemifield NumberField.RingOfIntegers.instIsFractionRing NormedField.toNorm NumberField.instNormedFieldValuedAdicCompletion DFunLike.coe RingHom WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid IsDedekindDomain.HeightOneSpectrum.valuation Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring WithVal.instField UniformSpace.Completion.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup RingHom.instFunLike embedding NumberField.RingOfIntegers.val NNReal.toReal MonoidWithZeroHom NNReal WithZero.instMulZeroOneClass Multiplicative.mulOneClass AddMonoid.toAddZeroClass Int.instAddMonoid NonAssocSemiring.toMulZeroOneClass instSemiringNNReal MonoidWithZeroHom.funLike WithZeroMulInt.toNNReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Ideal CommSemiring.toSemiring CommRing.toCommSemiring IdemSemiring.toSemiring Submodule.idemSemiring Nat.instMulZeroOneClass Ideal.absNorm NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instFreeInt IsDedekindDomain.HeightOneSpectrum.asIdeal NumberField.RingOfIntegers.HeightOneSpectrum.absNorm_ne_zero Valuation WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing Valuation.instFunLike IsDedekindDomain.HeightOneSpectrum.intValuation	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instIsFractionRing Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instFreeInt NumberField.RingOfIntegers.HeightOneSpectrum.absNorm_ne_zero Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing norm_def NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap
norm_embedding_eq 📖	mathematical	—	Norm.norm IsDedekindDomain.HeightOneSpectrum.adicCompletion NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Field.toSemifield NumberField.RingOfIntegers.instIsFractionRing maximalIdeal NormedField.toNorm NumberField.instNormedFieldValuedAdicCompletion DFunLike.coe RingHom WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid IsDedekindDomain.HeightOneSpectrum.valuation Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring WithVal.instField UniformSpace.Completion.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 Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup mk_maximalIdeal mk_apply
norm_eq_one_iff_notMem 📖	mathematical	—	Norm.norm IsDedekindDomain.HeightOneSpectrum.adicCompletion NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Field.toSemifield NumberField.RingOfIntegers.instIsFractionRing NormedField.toNorm NumberField.instNormedFieldValuedAdicCompletion DFunLike.coe RingHom WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid IsDedekindDomain.HeightOneSpectrum.valuation Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring WithVal.instField UniformSpace.Completion.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup RingHom.instFunLike embedding NumberField.RingOfIntegers.val Real Real.instOne Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule IsDedekindDomain.HeightOneSpectrum.asIdeal	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instIsFractionRing Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup norm_def IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_eq_one_iff NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instFreeInt NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal
norm_le_one 📖	mathematical	—	Real Real.instLE Norm.norm IsDedekindDomain.HeightOneSpectrum.adicCompletion NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Field.toSemifield NumberField.RingOfIntegers.instIsFractionRing NormedField.toNorm NumberField.instNormedFieldValuedAdicCompletion DFunLike.coe RingHom WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid IsDedekindDomain.HeightOneSpectrum.valuation Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring WithVal.instField UniformSpace.Completion.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup RingHom.instFunLike embedding NumberField.RingOfIntegers.val Real.instOne	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instIsFractionRing Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup norm_def IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_le_one NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instFreeInt NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal
norm_lt_one_iff_mem 📖	mathematical	—	Real Real.instLT Norm.norm IsDedekindDomain.HeightOneSpectrum.adicCompletion NumberField.RingOfIntegers NumberField.RingOfIntegers.instCommRing NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instAlgebra_1 DivisionRing.toRing Field.toDivisionRing Algebra.id Semifield.toCommSemiring Field.toSemifield NumberField.RingOfIntegers.instIsFractionRing NormedField.toNorm NumberField.instNormedFieldValuedAdicCompletion DFunLike.coe RingHom WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid IsDedekindDomain.HeightOneSpectrum.valuation Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring WithVal.instField UniformSpace.Completion.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup RingHom.instFunLike embedding NumberField.RingOfIntegers.val Real.instOne Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule IsDedekindDomain.HeightOneSpectrum.asIdeal	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instIsFractionRing Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup norm_def IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_lt_one_iff NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instFreeInt NumberField.RingOfIntegers.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.HeightOneSpectrum

Definitions

Name	Category	Theorems
adicAbv 📖	CompOp	7 math math: adicAbv_intCast_le_one, adicAbv_natCast_le_one, adicAbv_def, isNonarchimedean_adicAbv, NumberField.toNNReal_valued_eq_adicAbv, adicAbv_add_le_max, NumberField.FinitePlace.norm_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absNorm_ne_zero 📖	—	—	—	—	ne_zero_of_lt NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt 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 instSemiringNNReal MonoidWithZeroHom.funLike WithZeroMulInt.toNNReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Ideal NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass Ideal.absNorm NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt IsDedekindDomain.HeightOneSpectrum.asIdeal absNorm_ne_zero Valuation WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike IsDedekindDomain.HeightOneSpectrum.valuation NumberField.RingOfIntegers.instAlgebra_1 Semifield.toCommSemiring NumberField.RingOfIntegers.instIsFractionRing	—	—
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 MulRingSeminormClass.toAddGroupSeminormClass MulRingNormClass.toMulRingSeminormClass AbsoluteValue.instMulRingNormClassOfNontrivialOfIsDomain Real.instIsOrderedRing NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass IsLocalRing.toNontrivial Field.instIsLocalRing Real.instIsDomain MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass AbsoluteValue.monoidWithZeroHomClass 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
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 NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instIsFractionRing NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instFreeInt one_lt_absNorm_nnreal
one_lt_absNorm 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom Ideal NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike Ideal.absNorm NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt IsDedekindDomain.HeightOneSpectrum.asIdeal	—	NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt Ideal.IsPrime.ne_top IsDedekindDomain.HeightOneSpectrum.isPrime Ideal.absNorm_eq_one_iff Ideal.absNorm_ne_zero_iff Ideal.finiteQuotientOfFreeOfNeBot NumberField.RingOfIntegers.instIsDomain Module.IsNoetherian.finite NumberField.RingOfIntegers.instIsNoetherianInt IsDedekindDomain.HeightOneSpectrum.ne_bot
one_lt_absNorm_nnreal 📖	mathematical	—	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instOneNNReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instSemiringNNReal DFunLike.coe MonoidWithZeroHom Ideal NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing NonAssocSemiring.toMulZeroOneClass IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id Nat.instMulZeroOneClass MonoidWithZeroHom.funLike Ideal.absNorm NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt IsDedekindDomain.HeightOneSpectrum.asIdeal	—	NumberField.RingOfIntegers.instNontrivial NumberField.RingOfIntegers.instIsDedekindDomain NumberField.RingOfIntegers.instFreeInt Nat.cast_one NNReal.addLeftMono LinearOrderedCommMonoidWithZero.toZeroLeOneClass IsStrictOrderedRing.toCharZero NNReal.instIsStrictOrderedRing one_lt_absNorm

(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 IsTopologicalDivisionRing.toIsTopologicalRing Valued.valuedCompletion_apply Int.instAddLeftMono Int.instZeroLEOneClass Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid MonoidWithZeroHom.map_eq_zero_iff WithZero.instNontrivial
instIsDiscreteValuationRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation 📖	mathematical	—	IsDiscreteValuationRing Subring 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 SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid IsDedekindDomain.HeightOneSpectrum.valuation Subring.toCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Subring.instIsDomainSubtypeMem instIsDomain Field.toSemifield	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid Subring.instIsDomainSubtypeMem instIsDomain instIsPrincipalIdealRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation ValuationRing.isLocalRing Subring.instNontrivialSubtypeMem IsLocalRing.toNontrivial Field.instIsLocalRing ValuationRing.toPreValuationRing ValuationRing.instValuationRingInteger Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer Int.instZeroLEOneClass MonoidWithZeroHom.map_eq_zero_iff WithZero.instNontrivial Int.instAddLeftMono
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 UniformSpace.Completion.ring 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 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 SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid IsDedekindDomain.HeightOneSpectrum.valuation CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass 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