Integers

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

Statistics

Metric	Count
Definitions Integers, instAlgebraSubtypeMemSubringInteger, integer, leIdeal, leSubmodule, ltIdeal, ltSubmodule	7
Theorems not_isUnit_iff_valuation_lt_one, bijective_algebraMap_of_subsingleton_units_mrange, coe_span_singleton_eq_setOf_le_v_algebraMap, dvdNotUnit_iff_lt, dvd_iff_le, dvd_of_le, eq_algebraMap_or_inv_eq_algebraMap, exists_of_le_one, hom_inj, isPrincipal_iff_exists_eq_setOf_valuation_le, isPrincipal_iff_exists_isGreatest, isUnit_iff_valuation_eq_one, isUnit_of_one, isUnit_of_one', le_iff_dvd, le_of_dvd, map_le_one, nontrivial_iff, not_denselyOrdered_of_isPrincipalIdealRing, one_of_isUnit, one_of_isUnit', valuation_irreducible_lt_one, valuation_irreducible_pos, valuation_pos_iff_ne_zero, valuation_unit, coe_span_singleton_eq_setOf_le_v_coe, integers, v_irreducible_lt_one, v_irreducible_pos, integers_nontrivial, leIdeal_map_algebraMap_eq_leSubmodule_min, leIdeal_mono, leIdeal_v_le_of_mem, leIdeal_zero, leSubmodule_comap_algebraMap_eq_leIdeal, leSubmodule_monotone, leSubmodule_v_le_of_mem, leSubmodule_zero, ltIdeal_le_leIdeal, ltIdeal_mono, ltIdeal_v_le_of_mem, ltSubmodule_le_leSubmodule, ltSubmodule_monotone, ltSubmodule_v_le_of_mem, mem_integer_iff, mem_leIdeal_iff, mem_leSubmodule_iff, mem_ltIdeal_iff, mem_ltSubmodule_iff	49
Total	56

Valuation

Definitions

Name	Category	Theorems
Integers 📖	CompData	4 math math: IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, integer.integers, valuationSubring.integers, PadicComplexInt.integers
instAlgebraSubtypeMemSubringInteger 📖	CompOp	4 math math: leIdeal_map_algebraMap_eq_leSubmodule_min, integer.integers, leSubmodule_comap_algebraMap_eq_leIdeal, ValuationRing.instIsFractionRingInteger
integer 📖	CompOp	47 math math: ValuationRing.mem_integer_iff, ltIdeal_le_leIdeal, mem_leSubmodule_iff, mem_ltIdeal_iff, leSubmodule_monotone, instIsDiscreteValuationRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation, IsNonarchimedeanLocalField.instIsDiscreteValuationRingSubtypeMemSubringIntegerValueGroupWithZeroValuation, ValuationRing.range_algebraMap_eq, Integers.mem_of_integral, leIdeal_map_algebraMap_eq_leSubmodule_min, integer.integers, Integers.isIntegrallyClosed_integers, pow_Uniformizer_is_pow_generator, IsNonarchimedeanLocalField.instFiniteResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation, ltSubmodule_monotone, HasExtension.val_algebraMap, IsNonarchimedeanLocalField.instCompactSpaceSubtypeMemSubringIntegerValueGroupWithZeroValuation, Valued.isClosed_integer, HasExtension.instIsLocalHomValuationInteger, Valued.isClopen_integer, HasExtension.instIsTorsionFreeInteger, ltSubmodule_le_leSubmodule, leIdeal_mono, leIdeal_zero, integers_nontrivial, Integer.not_isUnit_iff_valuation_lt_one, exists_pow_Uniformizer, Valued.isOpen_integer, integer.coe_span_singleton_eq_setOf_le_v_coe, mem_ltSubmodule_iff, Valued.toNormedField.setOf_mem_integer_eq_closedBall, ValuationRing.instValuationRingInteger, mem_leIdeal_iff, Uniformizer.is_generator, ltIdeal_mono, ValuationRing.coe_equivInteger_apply, leSubmodule_zero, mem_integer_iff, IsNonarchimedeanLocalField.instCompleteSpaceSubtypeMemSubringIntegerValueGroupWithZeroValuation, leSubmodule_comap_algebraMap_eq_leIdeal, instIsPrincipalIdealRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation, ValuationSubring.integer_valuation, Uniformizer.valuation_gt_one, HasExtension.algebraMap_injective, ValuationRing.instIsFractionRingInteger, HasExtension.instIsScalarTowerInteger, HasExtension.val_smul
leIdeal 📖	CompOp	7 math math: ltIdeal_le_leIdeal, leIdeal_map_algebraMap_eq_leSubmodule_min, leIdeal_v_le_of_mem, leIdeal_mono, leIdeal_zero, mem_leIdeal_iff, leSubmodule_comap_algebraMap_eq_leIdeal
leSubmodule 📖	CompOp	7 math math: leSubmodule_v_le_of_mem, mem_leSubmodule_iff, leSubmodule_monotone, leIdeal_map_algebraMap_eq_leSubmodule_min, ltSubmodule_le_leSubmodule, leSubmodule_zero, leSubmodule_comap_algebraMap_eq_leIdeal
ltIdeal 📖	CompOp	4 math math: ltIdeal_le_leIdeal, mem_ltIdeal_iff, ltIdeal_v_le_of_mem, ltIdeal_mono
ltSubmodule 📖	CompOp	4 math math: ltSubmodule_monotone, ltSubmodule_le_leSubmodule, ltSubmodule_v_le_of_mem, mem_ltSubmodule_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integers_nontrivial 📖	mathematical	—	Nontrivial Subring CommRing.toRing SetLike.instMembership Subring.instSetLike integer	—	Integers.nontrivial_iff integer.integers
leIdeal_map_algebraMap_eq_leSubmodule_min 📖	mathematical	—	Submodule.map Subring DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subring.instSetLike integer CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass Subring.instSubringClass NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Semiring.toModule Algebra.toModule instAlgebraSubtypeMemSubringInteger Field.toCommRing RingHom.id RingHomSurjective.ids Algebra.linearMap leIdeal leSubmodule SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	Submodule.ext SubringClass.toSubsemiringClass Subring.instSubringClass RingHomSurjective.ids min_cases Subtype.prop LE.le.trans LT.lt.le
leIdeal_mono 📖	mathematical	—	Monotone Ideal Subring SetLike.instMembership Subring.instSetLike integer Ring.toSemiring Subring.toRing PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule leIdeal	—	LE.le.trans'
leIdeal_v_le_of_mem 📖	mathematical	Subring DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subring.instSetLike integer Ideal CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass Subring.instSubringClass Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	Ring.toSemiring Subring.toRing Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder leIdeal DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike	—	SubringClass.toSubsemiringClass Subring.instSubringClass AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass eq_or_ne map_zero MonoidWithZeroHomClass.toZeroHomClass ValuationClass.toMonoidWithZeroHomClass instValuationClass leIdeal_zero map_div₀ div_le_one_of_le₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE LinearOrderedCommMonoidWithZero.toMulPosStrictMono LinearOrderedCommMonoidWithZero.toZeroLeOneClass zero_le' div_mul_cancel₀ Iff.not ZeroMemClass.coe_eq_zero Submodule.smul_mem
leIdeal_zero 📖	mathematical	—	leIdeal DivisionRing.toRing Field.toDivisionRing MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero Bot.bot Ideal Subring SetLike.instMembership Subring.instSetLike integer Ring.toSemiring Subring.toRing Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Ideal.ext AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass SubringClass.toSubsemiringClass Subring.instSubringClass GroupWithZero.toNontrivial ValuationClass.toMonoidWithZeroHomClass instValuationClass
leSubmodule_comap_algebraMap_eq_leIdeal 📖	mathematical	—	Submodule.comap Subring DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subring.instSetLike integer CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass Subring.instSubringClass NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Semiring.toModule Algebra.toModule instAlgebraSubtypeMemSubringInteger Field.toCommRing RingHom.id Algebra.linearMap leSubmodule leIdeal	—	Submodule.ext SubringClass.toSubsemiringClass Subring.instSubringClass
leSubmodule_monotone 📖	mathematical	—	Monotone Submodule Subring SetLike.instMembership Subring.instSetLike integer Ring.toSemiring Subring.toRing NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subring.instModuleSubtypeMem Semiring.toModule PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Submodule.instPartialOrder leSubmodule	—	leAddSubgroup_monotone
leSubmodule_v_le_of_mem 📖	mathematical	Submodule Subring DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subring.instSetLike integer CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass Subring.instSubringClass NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Subring.instModuleSubtypeMem Semiring.toModule Ring.toSemiring Submodule.setLike	Subring.toRing NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder leSubmodule DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike	—	SubringClass.toSubsemiringClass Subring.instSubringClass eq_or_ne map_zero MonoidWithZeroHomClass.toZeroHomClass ValuationClass.toMonoidWithZeroHomClass instValuationClass leSubmodule_zero map_div₀ div_le_one_of_le₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE LinearOrderedCommMonoidWithZero.toMulPosStrictMono LinearOrderedCommMonoidWithZero.toZeroLeOneClass div_mul_cancel₀ Submodule.smul_mem
leSubmodule_zero 📖	mathematical	—	leSubmodule DivisionRing.toRing Field.toDivisionRing MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero Bot.bot Submodule Subring SetLike.instMembership Subring.instSetLike integer Ring.toSemiring Subring.toRing NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subring.instModuleSubtypeMem Semiring.toModule Submodule.instBot	—	Submodule.ext GroupWithZero.toNontrivial ValuationClass.toMonoidWithZeroHomClass instValuationClass
ltIdeal_le_leIdeal 📖	mathematical	—	Ideal Subring SetLike.instMembership Subring.instSetLike integer Ring.toSemiring Subring.toRing Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule ltIdeal leIdeal Units.val MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	LT.lt.le
ltIdeal_mono 📖	mathematical	—	Monotone Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero Ideal Subring SetLike.instMembership Subring.instSetLike integer Ring.toSemiring Subring.toRing Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule ltIdeal	—	LE.le.trans_lt' Units.val_le_val
ltIdeal_v_le_of_mem 📖	mathematical	Subring DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subring.instSetLike integer Ideal CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass Subring.instSubringClass Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	Ring.toSemiring Subring.toRing Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder ltIdeal CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike	—	SubringClass.toSubsemiringClass Subring.instSubringClass LE.le.trans' leIdeal_v_le_of_mem ltIdeal_le_leIdeal
ltSubmodule_le_leSubmodule 📖	mathematical	—	Submodule Subring SetLike.instMembership Subring.instSetLike integer Ring.toSemiring Subring.toRing NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subring.instModuleSubtypeMem Semiring.toModule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder ltSubmodule leSubmodule Units.val MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	ltAddSubgroup_le_leAddSubgroup
ltSubmodule_monotone 📖	mathematical	—	Monotone Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero Submodule Subring SetLike.instMembership Subring.instSetLike integer Ring.toSemiring Subring.toRing NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subring.instModuleSubtypeMem Semiring.toModule Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Submodule.instPartialOrder ltSubmodule	—	ltAddSubgroup_monotone
ltSubmodule_v_le_of_mem 📖	mathematical	Submodule Subring DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subring.instSetLike integer CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass Subring.instSubringClass NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Subring.instModuleSubtypeMem Semiring.toModule Ring.toSemiring Submodule.setLike	Subring.toRing NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder ltSubmodule CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero instFunLike	—	SubringClass.toSubsemiringClass Subring.instSubringClass LE.le.trans' leSubmodule_v_le_of_mem ltSubmodule_le_leSubmodule
mem_integer_iff 📖	mathematical	—	Subring SetLike.instMembership Subring.instSetLike integer Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	—
mem_leIdeal_iff 📖	mathematical	—	Subring SetLike.instMembership Subring.instSetLike integer Ideal Ring.toSemiring Subring.toRing Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule leIdeal Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation instFunLike	—	—
mem_leSubmodule_iff 📖	mathematical	—	Submodule Subring SetLike.instMembership Subring.instSetLike integer Ring.toSemiring Subring.toRing NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subring.instModuleSubtypeMem Semiring.toModule Submodule.setLike leSubmodule Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation instFunLike	—	—
mem_ltIdeal_iff 📖	mathematical	—	Subring SetLike.instMembership Subring.instSetLike integer Ideal Ring.toSemiring Subring.toRing Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule ltIdeal Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation instFunLike Units.val MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	—
mem_ltSubmodule_iff 📖	mathematical	—	Submodule Subring SetLike.instMembership Subring.instSetLike integer Ring.toSemiring Subring.toRing NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subring.instModuleSubtypeMem Semiring.toModule Submodule.setLike ltSubmodule Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation instFunLike Units.val MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	—

Valuation.Integer

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
not_isUnit_iff_valuation_lt_one 📖	mathematical	—	IsUnit Subring DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subring.instSetLike Valuation.integer MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass Subring.instSubringClass Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	SubringClass.toSubsemiringClass Subring.instSubringClass not_le not_iff_not Valuation.Integers.isUnit_iff_valuation_eq_one Valuation.integer.integers le_antisymm_iff

Valuation.Integers

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijective_algebraMap_of_subsingleton_units_mrange 📖	mathematical	Valuation.Integers Field.toCommRing	Function.Bijective DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap	—	MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass exists_of_le_one eq_or_ne map_zero MonoidWithZeroHomClass.toZeroHomClass Eq.le MonoidHom.instMonoidHomClass isUnit_iff_ne_zero
coe_span_singleton_eq_setOf_le_v_algebraMap 📖	mathematical	Valuation.Integers Field.toCommRing	SetLike.coe Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.span Set Set.instSingletonSet setOf Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike RingHom DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap	—	eq_or_ne Ideal.span_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass GroupWithZero.toNontrivial map_eq_zero_iff Set.ext dvd_iff_le
dvdNotUnit_iff_lt 📖	mathematical	Valuation.Integers Field.toCommRing	DvdNotUnit CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring 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	—	lt_iff_le_not_ge le_iff_dvd dvd_iff_le map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Mathlib.Tactic.Contrapose.contrapose₁ one_le_of_le_mul_left₀ PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono valuation_pos_iff_ne_zero ne_iff_lt_iff_le map_le_one isUnit_iff_valuation_eq_one dvdNotUnit_of_dvd_of_not_dvd
dvd_iff_le 📖	mathematical	Valuation.Integers Field.toCommRing	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Preorder.toLE 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	—	le_of_dvd dvd_of_le
dvd_of_le 📖	mathematical	Valuation.Integers Field.toCommRing Preorder.toLE 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	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing	—	by_cases Valuation.zero_iff GroupWithZero.toNontrivial le_zero_iff Valuation.map_zero RingHom.map_zero dvd_zero Valuation.map_one inv_mul_cancel₀ Valuation.map_mul le_imp_le_of_le_of_le mul_le_mul_right IsOrderedMonoid.toMulLeftMono LinearOrderedCommMonoidWithZero.toIsOrderedMonoid le_refl exists_of_le_one mul_inv_cancel_left₀ RingHom.map_mul
eq_algebraMap_or_inv_eq_algebraMap 📖	mathematical	Valuation.Integers Field.toCommRing	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	Valuation.val_le_one_or_val_inv_le_one exists_of_le_one
exists_of_le_one 📖	mathematical	Valuation.Integers Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation CommRing.toRing Valuation.instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	—	—
hom_inj 📖	mathematical	Valuation.Integers	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	—	—
isPrincipal_iff_exists_eq_setOf_valuation_le 📖	mathematical	Valuation.Integers Field.toCommRing	Submodule.IsPrincipal CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SetLike.coe Ideal Submodule.setLike setOf Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike RingHom DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap	—	isPrincipal_iff_exists_isGreatest Set.image_congr Set.ext Set.mem_image_of_mem Ideal.mem_of_dvd le_iff_dvd
isPrincipal_iff_exists_isGreatest 📖	mathematical	Valuation.Integers Field.toCommRing	Submodule.IsPrincipal CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsGreatest Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Set.image DFunLike.coe Valuation DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike RingHom DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap SetLike.coe Ideal Submodule.setLike	—	Set.mem_image_of_mem Set.image_congr le_of_dvd Ideal.ext dvd_of_le Ideal.mem_of_dvd
isUnit_iff_valuation_eq_one 📖	mathematical	Valuation.Integers Field.toCommRing	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	one_of_isUnit isUnit_of_one'
isUnit_of_one 📖	—	Valuation.Integers IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero CommRing.toRing Valuation.instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	—	map_le_one one_mul Valuation.map_mul Units.mul_inv Valuation.map_one le_refl exists_of_le_one map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Units.inv_mul
isUnit_of_one' 📖	mathematical	Valuation.Integers Field.toCommRing DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	isUnit_of_one Valuation.ne_zero_iff GroupWithZero.toNontrivial NeZero.one
le_iff_dvd 📖	mathematical	Valuation.Integers Field.toCommRing	Preorder.toLE 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 semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing	—	dvd_of_le le_of_dvd
le_of_dvd 📖	mathematical	Valuation.Integers semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation CommRing.toRing Valuation.instFunLike RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	—	mul_one map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Valuation.map_mul le_imp_le_of_le_of_le mul_le_mul_right IsOrderedMonoid.toMulLeftMono LinearOrderedCommMonoidWithZero.toIsOrderedMonoid map_le_one le_refl
map_le_one 📖	mathematical	Valuation.Integers	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation CommRing.toRing Valuation.instFunLike RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	—
nontrivial_iff 📖	mathematical	Valuation.Integers	Nontrivial	—	Function.Injective.nontrivial exists_of_le_one map_zero MonoidWithZeroHomClass.toZeroHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass NeZero.one
not_denselyOrdered_of_isPrincipalIdealRing 📖	mathematical	Valuation.Integers Field.toCommRing	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	—	map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Valuation.map_add_lt map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass LinearOrderedCommMonoidWithZero.toZeroLeOneClass NeZero.one GroupWithZero.toNontrivial map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass Right.mul_lt_one_of_le_of_lt covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono LinearOrderedCommMonoidWithZero.toIsOrderedMonoid map_le_one Set.image_congr isPrincipal_iff_exists_isGreatest IsPrincipalIdealRing.principal Set.mem_range_self Valuation.map_one DenselyOrdered.dense exists_of_le_one LT.lt.le LT.lt.not_ge
one_of_isUnit 📖	mathematical	Valuation.Integers IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero CommRing.toRing Valuation.instFunLike RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	one_of_isUnit' map_le_one
one_of_isUnit' 📖	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation CommRing.toRing Valuation.instFunLike RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	—	le_antisymm Valuation.map_one RingHom.map_one Units.mul_inv mul_one RingHom.map_mul Valuation.map_mul le_imp_le_of_le_of_le mul_le_mul_right IsOrderedMonoid.toMulLeftMono LinearOrderedCommMonoidWithZero.toIsOrderedMonoid le_refl
valuation_irreducible_lt_one 📖	mathematical	Valuation.Integers Field.toCommRing Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	lt_of_le_of_ne map_le_one isUnit_iff_valuation_eq_one Irreducible.not_isUnit
valuation_irreducible_pos 📖	mathematical	Valuation.Integers Field.toCommRing Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero DFunLike.coe Valuation DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap	—	valuation_pos_iff_ne_zero Irreducible.ne_zero
valuation_pos_iff_ne_zero 📖	mathematical	Valuation.Integers Field.toCommRing	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero DFunLike.coe Valuation DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap	—	not_le GroupWithZero.toNontrivial ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass map_eq_zero_iff MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
valuation_unit 📖	mathematical	Valuation.Integers Field.toCommRing	DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	isUnit_iff_valuation_eq_one

Valuation.integer

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_span_singleton_eq_setOf_le_v_coe 📖	mathematical	—	SetLike.coe Ideal Subring DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subring.instSetLike Valuation.integer CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass Subring.instSubringClass Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.span Set Set.instSingletonSet setOf Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike	—	Valuation.Integers.coe_span_singleton_eq_setOf_le_v_algebraMap integers
integers 📖	mathematical	—	Valuation.Integers Subring CommRing.toRing SetLike.instMembership Subring.instSetLike Valuation.integer Subring.toCommRing Valuation.instAlgebraSubtypeMemSubringInteger	—	Subtype.coe_injective
v_irreducible_lt_one 📖	mathematical	Irreducible Subring DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subring.instSetLike Valuation.integer MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass Subring.instSubringClass	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	SubringClass.toSubsemiringClass Subring.instSubringClass Valuation.Integers.valuation_irreducible_lt_one integers
v_irreducible_pos 📖	mathematical	Irreducible Subring DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subring.instSetLike Valuation.integer MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass Subring.instSubringClass	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero DFunLike.coe Valuation Valuation.instFunLike	—	SubringClass.toSubsemiringClass Subring.instSubringClass Valuation.Integers.valuation_irreducible_pos integers

---

← Back to Index