Archimedean

📁 Source: Mathlib/RingTheory/Valuation/Archimedean.lean

Statistics

Metric	Count
Definitions instLinearOrderedCommGroupWithZeroMrange, instLinearOrderedCommGroupWithZeroMrange	2
Theorems isPrincipalIdealRing_iff_not_denselyOrdered, isPrincipalIdealRing_iff_not_denselyOrdered_mrange, wellFounded_gt_on_v_iff_discrete_mrange, wfDvdMonoid_iff_wellFounded_gt_on_v	4
Total	6

MonoidWithZeroHom

Definitions

Name	Category	Theorems
instLinearOrderedCommGroupWithZeroMrange 📖	CompOp	—

Valuation

Definitions

Name	Category	Theorems
instLinearOrderedCommGroupWithZeroMrange 📖	CompOp	—

Valuation.Integers

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPrincipalIdealRing_iff_not_denselyOrdered 📖	mathematical	Valuation.Integers EuclideanDomain.toCommRing Field.toEuclideanDomain	IsPrincipalIdealRing CommSemiring.toSemiring CommRing.toCommSemiring DenselyOrdered Set.Elem Set.range DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder Set Set.instMembership	—	MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass not_denselyOrdered_of_isPrincipalIdealRing subsingleton_or_nontrivial bijective_algebraMap_of_subsingleton_units_mrange IsPrincipalIdealRing.of_surjective RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass EuclideanDomain.to_principal_ideal_domain RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass RingEquiv.surjective Function.Injective.isDomain instIsDomain RingHomClass.toMonoidWithZeroHomClass ValuationRing.of_integers List.TFAE.out IsBezout.TFAE ValuationRing.instIsBezout wfDvdMonoid_iff_wellFounded_gt_on_v wellFounded_gt_on_v_iff_discrete_mrange LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered
isPrincipalIdealRing_iff_not_denselyOrdered_mrange 📖	mathematical	Valuation.Integers EuclideanDomain.toCommRing Field.toEuclideanDomain	IsPrincipalIdealRing CommSemiring.toSemiring CommRing.toCommSemiring DenselyOrdered Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero SetLike.instMembership Submonoid.instSetLike MonoidHom.mrange NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike MonoidWithZeroHomClass.toMonoidHomClass Ring.toSemiring CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder	—	MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass isPrincipalIdealRing_iff_not_denselyOrdered
wellFounded_gt_on_v_iff_discrete_mrange 📖	mathematical	Valuation.Integers EuclideanDomain.toCommRing Field.toEuclideanDomain	Function.onFun Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap OrderMonoidIso Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero SetLike.instMembership Submonoid.instSetLike MonoidHom.mrange NonAssocSemiring.toMulZeroOneClass MonoidWithZeroHomClass.toMonoidHomClass Ring.toSemiring CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass WithZero Multiplicative Subtype.preorder WithZero.instPreorder Multiplicative.preorder instLatticeInt Submonoid.mul MulZeroClass.toMul WithZero.instMulZeroClass Multiplicative.mul	—	MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Set.wellFoundedOn_range Set.WellFoundedOn.mono' Set.WellFoundedOn.mapsTo exists_of_le_one map_le_one
wfDvdMonoid_iff_wellFounded_gt_on_v 📖	mathematical	Valuation.Integers EuclideanDomain.toCommRing Field.toEuclideanDomain	WfDvdMonoid CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring Function.onFun Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap	—	WellFounded.mono wellFounded_dvdNotUnit dvdNotUnit_iff_lt

---

← Back to Index