Basic

📁 Source: Mathlib/RingTheory/DiscreteValuationRing/Basic.lean

Statistics

Metric	Count
Definitions IsDiscreteValuationRing, HasUnitMulPowIrreducibleFactorization, addVal, quotient, remainder, toEuclideanDomain, toWithBotNat	7
Theorems addVal_pow, maximalIdeal_eq, maximalIdeal_eq_setOf_le_v_coe, maximalIdeal_pow_eq_setOf_le_v_coe_pow, of_ufd_of_unique_irreducible, toUniqueFactorizationMonoid, unique_irreducible, isDiscreteValuationRing, addVal_add, addVal_def, addVal_def', addVal_eq_top_iff, addVal_eq_zero_iff, addVal_eq_zero_of_unit, addVal_le_iff_dvd, addVal_mul, addVal_one, addVal_pow, addVal_uniformizer, addVal_zero, associated_of_irreducible, associated_pow_irreducible, aux_pid_of_ufd_of_unique_irreducible, bot_lt_toWithBotNat_iff, dvd_of_toWithBotNat_le_toWithBotNat, eq_unit_mul_pow_irreducible, exists_irreducible, exists_prime, ideal_eq_span_pow_irreducible, iff_pid_with_one_nonzero_prime, instIsHausdorffMaximalIdeal, irreducible_iff_uniformizer, irreducible_of_span_eq_maximalIdeal, not_a_field, not_a_field', not_isField, ofHasUnitMulPowIrreducibleFactorization, of_ufd_of_unique_irreducible, toIsLocalRing, toIsPrincipalIdealRing, toWithBotNat_eq_bot_iff, toWithBotNat_le_toWithBotNat_iff, toWithBotNat_zero, unit_mul_pow_congr_pow, unit_mul_pow_congr_unit, maximalIdeal_eq_setOf_le_v_algebraMap, maximalIdeal_pow_eq_setOf_le_v_algebraMap_pow, of_isDiscreteValuationRing	48
Total	55

Irreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addVal_pow 📖	mathematical	Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	DFunLike.coe AddValuation CommRing.toRing ENat instLinearOrderedAddCommMonoidWithTopENat AddValuation.instFunLike IsDiscreteValuationRing.addVal Monoid.toNatPow ENat.instNatCast	—	IsDiscreteValuationRing.addVal_pow IsDiscreteValuationRing.addVal_uniformizer nsmul_one
maximalIdeal_eq 📖	mathematical	Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	IsLocalRing.maximalIdeal IsDiscreteValuationRing.toIsLocalRing Ideal.span Set Set.instSingletonSet	—	IsDiscreteValuationRing.toIsLocalRing IsDiscreteValuationRing.irreducible_iff_uniformizer
maximalIdeal_eq_setOf_le_v_coe 📖	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	SetLike.coe Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal IsDiscreteValuationRing.toIsLocalRing Subring.toCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Subring.instIsDomainSubtypeMem instIsDomain setOf Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike	—	Subring.instIsDomainSubtypeMem instIsDomain SubringClass.toSubsemiringClass Subring.instSubringClass Valuation.Integers.maximalIdeal_eq_setOf_le_v_algebraMap Valuation.integer.integers
maximalIdeal_pow_eq_setOf_le_v_coe_pow 📖	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	SetLike.coe Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id IsLocalRing.maximalIdeal IsDiscreteValuationRing.toIsLocalRing Subring.toCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Subring.instIsDomainSubtypeMem instIsDomain setOf Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike Monoid.toNatPow GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	Subring.instIsDomainSubtypeMem instIsDomain SubringClass.toSubsemiringClass Subring.instSubringClass Valuation.Integers.maximalIdeal_pow_eq_setOf_le_v_algebraMap_pow Valuation.integer.integers

IsDiscreteValuationRing

Definitions

Name	Category	Theorems
HasUnitMulPowIrreducibleFactorization 📖	MathDef	2 math math: HasUnitMulPowIrreducibleFactorization.of_ufd_of_unique_irreducible, PowerSeries.hasUnitMulPowIrreducibleFactorization
addVal 📖	CompOp	13 math math: addVal_zero, addVal_def', Irreducible.addVal_pow, addVal_uniformizer, addVal_mul, addVal_add, addVal_pow, addVal_eq_zero_iff, addVal_eq_top_iff, addVal_eq_zero_of_unit, addVal_def, addVal_one, addVal_le_iff_dvd
quotient 📖	CompOp	—
remainder 📖	CompOp	—
toEuclideanDomain 📖	CompOp	—
toWithBotNat 📖	CompOp	4 math math: toWithBotNat_zero, bot_lt_toWithBotNat_iff, toWithBotNat_eq_bot_iff, toWithBotNat_le_toWithBotNat_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addVal_add 📖	mathematical	—	ENat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat SemilatticeInf.toMin DFunLike.coe AddValuation CommRing.toRing instLinearOrderedAddCommMonoidWithTopENat AddValuation.instFunLike addVal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	AddValuation.map_add
addVal_def 📖	mathematical	Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Units.val Monoid.toNatPow	DFunLike.coe AddValuation CommRing.toRing ENat instLinearOrderedAddCommMonoidWithTopENat AddValuation.instFunLike addVal ENat.instNatCast	—	exists_prime addVal.eq_1 multiplicity_addValuation_apply emultiplicity_eq_of_associated_left associated_of_irreducible Prime.irreducible IsDomain.toIsCancelMulZero emultiplicity_eq_of_associated_right Associated.symm mul_comm emultiplicity_pow_self_of_prime irreducible_iff_prime UniqueFactorizationMonoid.instDecompositionMonoid PrincipalIdealRing.to_uniqueFactorizationMonoid toIsPrincipalIdealRing
addVal_def' 📖	mathematical	Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	DFunLike.coe AddValuation CommRing.toRing ENat instLinearOrderedAddCommMonoidWithTopENat AddValuation.instFunLike addVal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Units.val Monoid.toNatPow ENat.instNatCast	—	addVal_def
addVal_eq_top_iff 📖	mathematical	—	DFunLike.coe AddValuation CommRing.toRing ENat instLinearOrderedAddCommMonoidWithTopENat AddValuation.instFunLike addVal Top.top instTopENat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	exists_prime Prime.irreducible IsDomain.toIsCancelMulZero Mathlib.Tactic.Contrapose.contrapose₁ associated_pow_irreducible Associated.symm mul_comm addVal_def' addVal_zero
addVal_eq_zero_iff 📖	mathematical	—	DFunLike.coe AddValuation CommRing.toRing ENat instLinearOrderedAddCommMonoidWithTopENat AddValuation.instFunLike addVal instZeroENat IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	eq_or_ne AddValuation.map_zero NeZero.one IsLocalRing.toNontrivial toIsLocalRing exists_irreducible eq_unit_mul_pow_irreducible AddValuation.map_mul addVal_eq_zero_of_unit AddValuation.map_pow addVal_uniformizer nsmul_eq_mul mul_one zero_add instIsDedekindFiniteMonoid isUnit_pow_iff_of_not_isUnit Irreducible.not_isUnit
addVal_eq_zero_of_unit 📖	mathematical	—	DFunLike.coe AddValuation CommRing.toRing ENat instLinearOrderedAddCommMonoidWithTopENat AddValuation.instFunLike addVal Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instZeroENat	—	exists_irreducible addVal_def pow_zero mul_one CharP.cast_eq_zero CharP.ofCharZero
addVal_le_iff_dvd 📖	mathematical	—	ENat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat DFunLike.coe AddValuation CommRing.toRing instLinearOrderedAddCommMonoidWithTopENat AddValuation.instFunLike addVal semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing	—	exists_prime addVal_eq_top_iff top_le_iff addVal_zero dvd_zero associated_pow_irreducible Prime.irreducible IsDomain.toIsCancelMulZero Dvd.dvd.trans Associated.dvd emultiplicity_le_emultiplicity_iff multiplicity_addValuation_apply addVal.eq_1 Associated.symm emultiplicity_le_emultiplicity_of_dvd_right
addVal_mul 📖	mathematical	—	DFunLike.coe AddValuation CommRing.toRing ENat instLinearOrderedAddCommMonoidWithTopENat AddValuation.instFunLike addVal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	AddValuation.map_mul
addVal_one 📖	mathematical	—	DFunLike.coe AddValuation CommRing.toRing ENat instLinearOrderedAddCommMonoidWithTopENat AddValuation.instFunLike addVal AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instZeroENat	—	AddValuation.map_one
addVal_pow 📖	mathematical	—	DFunLike.coe AddValuation CommRing.toRing ENat instLinearOrderedAddCommMonoidWithTopENat AddValuation.instFunLike addVal Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instCommSemiringENat	—	AddValuation.map_pow
addVal_uniformizer 📖	mathematical	Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	DFunLike.coe AddValuation CommRing.toRing ENat instLinearOrderedAddCommMonoidWithTopENat AddValuation.instFunLike addVal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instCommSemiringENat	—	pow_one one_mul Nat.cast_one addVal_def
addVal_zero 📖	mathematical	—	DFunLike.coe AddValuation CommRing.toRing ENat instLinearOrderedAddCommMonoidWithTopENat AddValuation.instFunLike addVal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Top.top instTopENat	—	AddValuation.map_zero
associated_of_irreducible 📖	mathematical	Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	Associated	—	Ideal.span_singleton_eq_span_singleton toIsLocalRing irreducible_iff_uniformizer
associated_pow_irreducible 📖	mathematical	Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	Associated Monoid.toNatPow	—	IsNoetherianRing.wfDvdMonoid PrincipalIdealRing.isNoetherianRing toIsPrincipalIdealRing WfDvdMonoid.exists_factors Associates.mk_eq_mk_iff_associated Associates.mk_pow Multiset.prod_replicate Multiset.eq_replicate Multiset.card_map associated_of_irreducible
aux_pid_of_ufd_of_unique_irreducible 📖	mathematical	Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Associated	IsPrincipalIdealRing	—	Submodule.span_zero Submodule.ne_bot_iff HasUnitMulPowIrreducibleFactorization.of_ufd_of_unique_irreducible Units.mul_inv_cancel_right Ideal.mul_mem_right Ideal.instIsTwoSided_1 le_antisymm pow_dvd_pow Nat.find_min' Ideal.span_singleton_le_iff_mem Nat.find_spec
bot_lt_toWithBotNat_iff 📖	mathematical	—	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder Bot.bot WithBot.bot toWithBotNat	—	bot_lt_iff_ne_bot
dvd_of_toWithBotNat_le_toWithBotNat 📖	mathematical	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder toWithBotNat	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing	—	toWithBotNat.congr_simp toWithBotNat_zero toWithBotNat_le_toWithBotNat_iff
eq_unit_mul_pow_irreducible 📖	mathematical	Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Units.val Monoid.toNatPow	—	associated_pow_irreducible Associated.symm mul_comm
exists_irreducible 📖	mathematical	—	Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	toIsLocalRing Submodule.IsPrincipal.principal IsPrincipalIdealRing.principal toIsPrincipalIdealRing
exists_prime 📖	mathematical	—	Prime CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring	—	irreducible_iff_prime IsDomain.toIsCancelMulZero UniqueFactorizationMonoid.instDecompositionMonoid PrincipalIdealRing.to_uniqueFactorizationMonoid toIsPrincipalIdealRing exists_irreducible
ideal_eq_span_pow_irreducible 📖	mathematical	Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	Ideal.span Set Set.instSingletonSet Monoid.toNatPow	—	IsPrincipalIdealRing.principal toIsPrincipalIdealRing Submodule.IsPrincipal.eq_bot_iff_generator_eq_zero associated_pow_irreducible Ideal.span_singleton_generator Ideal.span_singleton_eq_span_singleton
iff_pid_with_one_nonzero_prime 📖	mathematical	—	IsDiscreteValuationRing IsPrincipalIdealRing CommSemiring.toSemiring CommRing.toCommSemiring ExistsUnique Ideal Bot.bot Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.IsPrime	—	Ideal.IsMaximal.isPrime' IsLocalRing.maximalIdeal.isMaximal Submodule.IsPrincipal.principal IsPrincipalIdealRing.principal Ideal.span_singleton_zero Prime.irreducible IsDomain.toIsCancelMulZero Ideal.span_singleton_prime Ideal.submodule_span_eq toIsLocalRing irreducible_iff_uniformizer IsLocalRing.of_unique_nonzero_prime IsLocalRing.le_maximalIdeal Ideal.IsPrime.ne_top' le_antisymm le_trans le_of_eq le_refl bot_le
instIsHausdorffMaximalIdeal 📖	mathematical	—	IsHausdorff IsLocalRing.maximalIdeal CommRing.toCommSemiring toIsLocalRing Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring	—	toIsLocalRing IsScalarTower.left IsScalarTower.right exists_irreducible addVal_eq_top_iff WithTop.eq_top_iff_forall_ge instNoTopOrderOfNoMaxOrder Nat.instNoMaxOrder Irreducible.maximalIdeal_eq Ideal.span_singleton_pow Ideal.instIsTwoSided_1 mul_one Irreducible.addVal_pow
irreducible_iff_uniformizer 📖	mathematical	—	Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring IsLocalRing.maximalIdeal toIsLocalRing Ideal.span Set Set.instSingletonSet	—	toIsLocalRing IsLocalRing.eq_maximalIdeal PrincipalIdealRing.isMaximal_of_irreducible toIsPrincipalIdealRing irreducible_of_span_eq_maximalIdeal not_a_field Ideal.span_singleton_eq_bot
irreducible_of_span_eq_maximalIdeal 📖	mathematical	IsLocalRing.maximalIdeal Ideal.span CommSemiring.toSemiring Set Set.instSingletonSet	Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Submodule.mem_span_singleton_self Ideal.mem_span_singleton' eq_zero_of_mul_eq_self_right IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero isUnit_of_dvd_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw
not_a_field 📖	—	—	—	—	not_a_field'
not_a_field' 📖	—	—	—	—	—
not_isField 📖	mathematical	—	IsField CommSemiring.toSemiring CommRing.toCommSemiring	—	toIsLocalRing Iff.not IsLocalRing.isField_iff_maximalIdeal_eq not_a_field
ofHasUnitMulPowIrreducibleFactorization 📖	mathematical	HasUnitMulPowIrreducibleFactorization	IsDiscreteValuationRing	—	of_ufd_of_unique_irreducible HasUnitMulPowIrreducibleFactorization.toUniqueFactorizationMonoid IsDomain.toIsCancelMulZero HasUnitMulPowIrreducibleFactorization.unique_irreducible
of_ufd_of_unique_irreducible 📖	mathematical	Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Associated	IsDiscreteValuationRing	—	iff_pid_with_one_nonzero_prime aux_pid_of_ufd_of_unique_irreducible Submodule.ne_bot_iff Ideal.mem_span_singleton dvd_refl Irreducible.ne_zero Ideal.span_singleton_prime UniqueFactorizationMonoid.irreducible_iff_prime IsPrincipalIdealRing.principal Submodule.IsPrincipal.span_singleton_generator Ideal.span_singleton_eq_span_singleton Submodule.span_singleton_eq_bot
toIsLocalRing 📖	mathematical	—	IsLocalRing CommSemiring.toSemiring CommRing.toCommSemiring	—	—
toIsPrincipalIdealRing 📖	mathematical	—	IsPrincipalIdealRing CommSemiring.toSemiring CommRing.toCommSemiring	—	—
toWithBotNat_eq_bot_iff 📖	mathematical	—	toWithBotNat Bot.bot WithBot WithBot.bot MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	addVal_eq_top_iff
toWithBotNat_le_toWithBotNat_iff 📖	mathematical	—	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder toWithBotNat semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing	—	addVal_eq_top_iff addVal_le_iff_dvd WithBot.coe_le_coe WithTop.coe_le_coe
toWithBotNat_zero 📖	mathematical	—	toWithBotNat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Bot.bot WithBot WithBot.bot	—	addVal_zero
unit_mul_pow_congr_pow 📖	—	Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Units.val Monoid.toNatPow	—	—	Multiset.prod_replicate Associated.eq_1 mul_left_comm mul_assoc mul_right_comm Units.mul_inv one_mul Multiset.card_eq_card_of_rel UniqueFactorizationMonoid.factors_unique PrincipalIdealRing.to_uniqueFactorizationMonoid toIsPrincipalIdealRing Multiset.eq_of_mem_replicate Multiset.card_replicate
unit_mul_pow_congr_unit 📖	—	Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Units.val Monoid.toNatPow	—	—	mul_eq_zero IsDomain.to_noZeroDivisors sub_mul sub_eq_zero Irreducible.ne_zero eq_zero_of_pow_eq_zero isReduced_of_noZeroDivisors unit_mul_pow_congr_pow

IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_ufd_of_unique_irreducible 📖	mathematical	Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Associated	IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization	—	WfDvdMonoid.exists_factors UniqueFactorizationMonoid.toIsWellFounded Associates.mk_eq_mk_iff_associated Associates.mk_pow Multiset.prod_replicate Multiset.eq_replicate Multiset.card_map
toUniqueFactorizationMonoid 📖	mathematical	IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization	UniqueFactorizationMonoid CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring	—	UniqueFactorizationMonoid.of_exists_prime_factors Multiset.eq_of_mem_replicate Irreducible.ne_zero Irreducible.not_isUnit Units.dvd_mul_right pow_zero one_mul Units.dvd_mul_left mul_left_comm mul_assoc pow_succ' dvd_mul_of_dvd_left dvd_rfl Multiset.prod_replicate
unique_irreducible 📖	mathematical	IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	Associated	—	Irreducible.ne_zero Associated.irreducible Associated.symm lt_trichotomy pow_zero pow_one Irreducible.isUnit_or_isUnit pow_succ' Irreducible.not_isUnit isUnit_of_mul_isUnit_left instIsDedekindFiniteMonoid add_comm Associated.trans

IsDiscreteValuationRing.RingEquivClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isDiscreteValuationRing 📖	mathematical	—	IsDiscreteValuationRing	—	RingEquiv.isLocalRing IsDiscreteValuationRing.toIsLocalRing isPrincipalIdealRing_iff IsPrincipalIdealRing.of_surjective RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass IsDiscreteValuationRing.toIsPrincipalIdealRing RingEquiv.surjective Submodule.nonzero_mem_of_bot_lt bot_lt_iff_ne_bot IsDiscreteValuationRing.not_a_field Submodule.ne_bot_iff IsLocalRing.mem_maximalIdeal map_mem_nonunits_iff MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass isLocalHom_equiv RingEquivClass.toMulEquivClass EquivLike.toEmbeddingLike MonoidWithZeroHomClass.toZeroHomClass AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass

Valuation.Integers

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
maximalIdeal_eq_setOf_le_v_algebraMap 📖	mathematical	Valuation.Integers EuclideanDomain.toCommRing Field.toEuclideanDomain Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	SetLike.coe Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal IsDiscreteValuationRing.toIsLocalRing Function.Injective.isDomain DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instIsDomain RingHom RingHom.instFunLike RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass algebraMap 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	—	Function.Injective.isDomain instIsDomain RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsDiscreteValuationRing.toIsLocalRing coe_span_singleton_eq_setOf_le_v_algebraMap Irreducible.maximalIdeal_eq
maximalIdeal_pow_eq_setOf_le_v_algebraMap_pow 📖	mathematical	Valuation.Integers EuclideanDomain.toCommRing Field.toEuclideanDomain Irreducible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	SetLike.coe Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id IsLocalRing.maximalIdeal IsDiscreteValuationRing.toIsLocalRing Function.Injective.isDomain DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instIsDomain RingHom RingHom.instFunLike RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass algebraMap 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 Monoid.toNatPow GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	Function.Injective.isDomain instIsDomain RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass IsScalarTower.right IsDiscreteValuationRing.toIsLocalRing coe_span_singleton_eq_setOf_le_v_algebraMap IsScalarTower.left Ideal.span_singleton_pow Ideal.instIsTwoSided_1 Irreducible.maximalIdeal_eq

(root)

Definitions

Name	Category	Theorems
IsDiscreteValuationRing 📖	CompData	18 math math: IsDiscreteValuationRing.ofHasUnitMulPowIrreducibleFactorization, IsLocalRing.finrank_CotangentSpace_eq_one_iff, Valued.integer.compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField, instIsDiscreteValuationRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation, IsNonarchimedeanLocalField.instIsDiscreteValuationRingSubtypeMemSubringIntegerValueGroupWithZeroValuation, PadicInt.instIsDiscreteValuationRing, IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain, Valuation.valuationSubring_isDiscreteValuationRing, WittVector.isDiscreteValuationRing, Valued.integer.properSpace_iff_completeSpace_and_isDiscreteValuationRing_integer_and_finite_residueField, IsDedekindDomainDvr.is_dvr_at_nonzero_prime, IsDiscreteValuationRing.RingEquivClass.isDiscreteValuationRing, PowerSeries.instIsDiscreteValuationRing, Valued.integer.isDiscreteValuationRing_of_compactSpace, instIsDiscreteValuationRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, IsDiscreteValuationRing.TFAE, IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime, IsDiscreteValuationRing.of_ufd_of_unique_irreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isDiscreteValuationRing 📖	mathematical	—	ValuationRing	—	ValuationRing.instOfIsLocalRingOfIsBezout IsDiscreteValuationRing.toIsLocalRing IsBezout.of_isPrincipalIdealRing IsDiscreteValuationRing.toIsPrincipalIdealRing

---

← Back to Index