ValuationRing

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

Statistics

Metric	Count
Definitions `PreValuationRing`, `ValuationRing`, `ValueGroup`, `commGroupWithZero`, `equivInteger`, `instInhabitedValueGroup`, `instInvValueGroup`, `instLEValueGroup`, `instLinearOrderIdealOfDecidableLE`, `instMulValueGroup`, `instOneValueGroup`, `instZeroValueGroup`, `linearOrder`, `linearOrderedCommGroupWithZero`, `valuation`	15
Theorems `preValuationRing`, `valuationRing`, `cond`, `cond'`, `iff_dvd_total`, `iff_ideal_total`, `isFractionRing`, `coe_equivInteger_apply`, `cond`, `dvd_total`, `iff_dvd_total`, `iff_ideal_total`, `iff_isInteger_or_isInteger`, `iff_local_bezout_domain`, `instIsBezout`, `instIsFractionRingInteger`, `instNontrivialValueGroup`, `instOfIsLocalRingOfIsBezout`, `instValuationRingInteger`, `isFractionRing_iff`, `isInteger_or_isInteger`, `isLocalRing`, `le_total`, `le_total_ideal`, `mem_integer_iff`, `of_field`, `of_integers`, `range_algebraMap_eq`, `toPreValuationRing`, `unique_irreducible`, `isFractionRing_of_exists_eq_algebraMap_or_inv_eq_algebraMap_of_injective`	31
Total	46

Function.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preValuationRing` 📖	mathematical	`DFunLike.coe` `MulHom` `MulHom.funLike`	`PreValuationRing`	—	`PreValuationRing.cond` `map_mul` `MulHom.mulHomClass`
`valuationRing` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	`ValuationRing`	—	`preValuationRing` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass`

PreValuationRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cond` 📖	—	—	—	—	`cond'`
`cond'` 📖	—	—	—	—	—
`iff_dvd_total` 📖	mathematical	—	`PreValuationRing` `Semigroup.toMul` `semigroupDvd`	—	`cond`
`iff_ideal_total` 📖	mathematical	—	`PreValuationRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`le_total` `iff_dvd_total`

Valuation.Integers

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isFractionRing` 📖	mathematical	`Valuation.Integers` `Field.toCommRing`	`IsFractionRing` `CommRing.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield`	—	`isFractionRing_of_exists_eq_algebraMap_or_inv_eq_algebraMap_of_injective` `eq_algebraMap_or_inv_eq_algebraMap`

ValuationRing

Definitions

Name	Category	Theorems
`ValueGroup` 📖	CompOp	5 math math: `mem_integer_iff`, `range_algebraMap_eq`, `instNontrivialValueGroup`, `le_total`, `coe_equivInteger_apply`
`commGroupWithZero` 📖	CompOp	—
`equivInteger` 📖	CompOp	1 math math: `coe_equivInteger_apply`
`instInhabitedValueGroup` 📖	CompOp	—
`instInvValueGroup` 📖	CompOp	—
`instLEValueGroup` 📖	CompOp	1 math math: `le_total`
`instLinearOrderIdealOfDecidableLE` 📖	CompOp	—
`instMulValueGroup` 📖	CompOp	—
`instOneValueGroup` 📖	CompOp	—
`instZeroValueGroup` 📖	CompOp	—
`linearOrder` 📖	CompOp	—
`linearOrderedCommGroupWithZero` 📖	CompOp	3 math math: `mem_integer_iff`, `range_algebraMap_eq`, `coe_equivInteger_apply`
`valuation` 📖	CompOp	3 math math: `mem_integer_iff`, `range_algebraMap_eq`, `coe_equivInteger_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_equivInteger_apply` 📖	mathematical	—	`Subring` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subring.instSetLike` `Valuation.integer` `ValueGroup` `linearOrderedCommGroupWithZero` `valuation` `DFunLike.coe` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Subring.toCommRing` `Field.toCommRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `equivInteger` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap`	—	—
`cond` 📖	—	—	—	—	`PreValuationRing.cond`
`dvd_total` 📖	mathematical	—	`semigroupDvd`	—	`PreValuationRing.iff_dvd_total`
`iff_dvd_total` 📖	mathematical	—	`ValuationRing` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing`	—	`toPreValuationRing` `PreValuationRing.iff_dvd_total`
`iff_ideal_total` 📖	mathematical	—	`ValuationRing` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`toPreValuationRing` `PreValuationRing.iff_ideal_total`
`iff_isInteger_or_isInteger` 📖	mathematical	—	`ValuationRing` `IsLocalization.IsInteger` `CommRing.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero`	—	`IsFractionRing.div_surjective` `map_ne_zero_iff` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsFractionRing.injective` `nonZeroDivisors.ne_zero` `IsDomain.toNontrivial` `cond` `toPreValuationRing` `eq_inv_of_mul_eq_one_left` `mul_div` `div_eq_one_iff_eq` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `mul_comm` `eq_div_iff` `MulZeroClass.mul_zero` `inv_div`
`iff_local_bezout_domain` 📖	mathematical	—	`ValuationRing` `IsLocalRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsBezout`	—	`isLocalRing` `IsDomain.toNontrivial` `toPreValuationRing` `instIsBezout` `instOfIsLocalRingOfIsBezout`
`instIsBezout` 📖	mathematical	—	`IsBezout` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`IsBezout.iff_span_pair_isPrincipal` `Ideal.span_insert` `toPreValuationRing` `le_total` `sup_eq_right` `sup_eq_left`
`instIsFractionRingInteger` 📖	mathematical	—	`IsFractionRing` `Subring` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subring.instSetLike` `Valuation.integer` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `Valuation.instAlgebraSubtypeMemSubringInteger` `Field.toCommRing`	—	`Valuation.Integers.isFractionRing` `Valuation.integer.integers`
`instNontrivialValueGroup` 📖	mathematical	—	`Nontrivial` `ValueGroup`	—	`Quotient.exact'` `inv_smul_smul` `smul_zero` `NeZero.one` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing`
`instOfIsLocalRingOfIsBezout` 📖	mathematical	—	`ValuationRing`	—	`iff_dvd_total` `IsBezout.span_pair_isPrincipal` `Ideal.mem_span_singleton'` `Ideal.subset_span` `Ideal.mem_span_pair` `eq_or_ne` `MulZeroClass.mul_zero` `mul_left_injective₀` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_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.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `IsLocalRing.isUnit_or_isUnit_of_add_one` `mul_dvd_mul_right` `isUnit_iff_forall_dvd` `isUnit_of_mul_isUnit_right` `instIsDedekindFiniteMonoid`
`instValuationRingInteger` 📖	mathematical	—	`ValuationRing` `Subring` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subring.instSetLike` `Valuation.integer` `Subring.toCommRing` `Field.toCommRing` `Subring.instIsDomainSubtypeMem` `instIsDomain` `Field.toSemifield`	—	`of_integers` `Valuation.integer.integers`
`isFractionRing_iff` 📖	mathematical	—	`IsFractionRing` `CommRing.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero`	—	`isInteger_or_isInteger` `IsFractionRing.injective` `isFractionRing_of_exists_eq_algebraMap_or_inv_eq_algebraMap_of_injective`
`isInteger_or_isInteger` 📖	mathematical	—	`IsLocalization.IsInteger` `CommRing.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero`	—	`iff_isInteger_or_isInteger`
`isLocalRing` 📖	mathematical	—	`IsLocalRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`IsLocalRing.of_isUnit_or_isUnit_one_sub_self` `PreValuationRing.cond` `IsUnit.of_mul_eq_one` `instIsDedekindFiniteMonoid` `mul_add` `Distrib.leftDistribClass` `mul_one` `sub_add_cancel` `add_sub_cancel`
`le_total` 📖	mathematical	—	`ValueGroup` `instLEValueGroup`	—	`IsFractionRing.div_surjective` `IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors` `IsDomain.toNontrivial` `cond` `toPreValuationRing` `Algebra.smul_def` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `Mathlib.Tactic.LinearCombination.eq_of_eq` `AddRightCancelSemigroup.toIsRightCancelAdd` `Mathlib.Tactic.LinearCombination.eq_rearrange` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `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.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `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_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero`
`le_total_ideal` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`Mathlib.Tactic.Push.not_forall_eq` `PreValuationRing.cond` `Ideal.mul_mem_right` `Ideal.instIsTwoSided_1`
`mem_integer_iff` 📖	mathematical	—	`Subring` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subring.instSetLike` `Valuation.integer` `ValueGroup` `linearOrderedCommGroupWithZero` `valuation` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap`	—	`Algebra.smul_def` `mul_one`
`of_field` 📖	mathematical	—	`ValuationRing` `Field.toCommRing` `instIsDomain` `Field.toSemifield`	—	`instIsDomain` `instOfIsLocalRingOfIsBezout` `Field.instIsLocalRing` `IsBezout.of_isPrincipalIdealRing` `EuclideanDomain.to_principal_ideal_domain`
`of_integers` 📖	mathematical	`Valuation.Integers` `Field.toCommRing`	`ValuationRing` `Function.Injective.isDomain` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instIsDomain` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `algebraMap`	—	`le_total` `Valuation.Integers.dvd_of_le` `Function.Injective.isDomain` `instIsDomain` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`range_algebraMap_eq` 📖	mathematical	—	`Valuation.integer` `ValueGroup` `DivisionRing.toRing` `Field.toDivisionRing` `linearOrderedCommGroupWithZero` `valuation` `RingHom.range` `CommRing.toRing` `algebraMap` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`Subring.ext` `mem_integer_iff`
`toPreValuationRing` 📖	mathematical	—	`PreValuationRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	—
`unique_irreducible` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Associated`	—	`dvd_total` `associated_of_dvd_dvd` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `Irreducible.dvd_symm` `Irreducible.dvd_comm`

(root)

Definitions

Name	Category	Theorems
`PreValuationRing` 📖	CompData	4 math math: `ValuationRing.toPreValuationRing`, `PreValuationRing.iff_dvd_total`, `PreValuationRing.iff_ideal_total`, `Function.Surjective.preValuationRing`
`ValuationRing` 📖	CompData	16 math math: `AlgebraicGeometry.ValuativeCommSq.valuationRing`, `ValuationRing.TFAE`, `ValuationRing.iff_isInteger_or_isInteger`, `ValuationRing.instOfIsLocalRingOfIsBezout`, `ArchimedeanClass.FiniteElement.instValuationRing`, `tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain`, `of_isDiscreteValuationRing`, `ValuationSubring.instValuationRingSubtypeMem`, `ValuationRing.iff_local_bezout_domain`, `ValuationRing.of_integers`, `ValuationRing.iff_ideal_total`, `IsDiscreteValuationRing.TFAE`, `Function.Surjective.valuationRing`, `ValuationRing.instValuationRingInteger`, `ValuationRing.iff_dvd_total`, `ValuationRing.of_field`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isFractionRing_of_exists_eq_algebraMap_or_inv_eq_algebraMap_of_injective` 📖	mathematical	`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`	`IsFractionRing` `Semifield.toCommSemiring`	—	`Function.Injective.isDomain` `instIsDomain` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `faithfulSMul_iff_algebraMap_injective` `IsDomain.of_faithfulSMul` `IsDomain.toNontrivial` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `mul_one` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `eq_div_iff` `one_div` `inv_eq_iff_eq_inv` `mem_nonZeroDivisors_of_ne_zero` `IsDomain.to_noZeroDivisors` `one_mul`

---

← Back to Index