Documentation Verification Report

Basic

📁 Source: Mathlib/RingTheory/Valuation/Discrete/Basic.lean

Statistics

Metric	Count
Definitions `equivValuationSubring`, `maximalIdeal`, `IsRankOneDiscrete`, `generator`, `IsUniformizer`, `Uniformizer`, `instCoeSubtypeMemSubringInteger`, `mk'`, `val`	9
Theorems `exists_lift_of_le_one`, `isRankOneDiscrete`, `map_algebraMap_eq_valuationSubring`, `exists_generator_lt_one`, `exists_generator_lt_one'`, `generator_lt_one`, `generator_mem_range`, `generator_mem_valueGroup`, `generator_ne_one`, `generator_ne_zero`, `generator_zpowers_eq_range`, `generator_zpowers_eq_valueGroup`, `instIsCyclicSubtypeUnitsMemSubgroupValueGroup`, `instIsNontrivial`, `mk'`, `valueGroup_genLTOne_eq_generator`, `iff`, `is_generator`, `ne_zero`, `not_isUnit`, `of_associated`, `val`, `val_lt_one`, `val_ne_zero`, `val_pos`, `zpowers_eq_valueGroup`, `ext`, `ext_iff`, `is_generator`, `ne_zero`, `valuation_gt_one`, `associated_of_isUniformizer`, `exists_isUniformizer_of_isCyclic_of_nontrivial`, `exists_pow_Uniformizer`, `ideal_isPrincipal`, `instNonemptyUniformizer`, `isUniformizer_of_maximalIdeal_eq_span`, `pow_Uniformizer_is_pow_generator`, `valuationSubring_isDiscreteValuationRing`, `valuationSubring_isPrincipalIdealRing`, `valuationSubring_not_isField`	41
Total	50

IsDiscreteValuationRing

Definitions

Name	Category	Theorems
`equivValuationSubring` 📖	CompOp	—
`maximalIdeal` 📖	CompOp	5 math math: `WeierstrassCurve.valuation_Δ_aux_eq_of_isIntegral`, `isRankOneDiscrete`, `WeierstrassCurve.isGoodReduction_iff`, `map_algebraMap_eq_valuationSubring`, `WeierstrassCurve.IsGoodReduction.goodReduction`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_lift_of_le_one` 📖	mathematical	`WithZero` `Multiplicative` `Preorder.toLE` `WithZero.instPreorder` `Multiplicative.preorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `DFunLike.coe` `Valuation` `WithZero.instLinearOrderedCommMonoidWithZero` `Multiplicative.commMonoid` `Int.instAddCommMonoid` `Multiplicative.linearOrder` `Int.instLinearOrder` `Multiplicative.isOrderedCancelMonoid` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `Int.instIsStrictOrderedRing` `DivisionRing.toRing` `Field.toDivisionRing` `Valuation.instFunLike` `IsDedekindDomain.HeightOneSpectrum.valuation` `IsPrincipalIdealRing.isDedekindDomain` `toIsPrincipalIdealRing` `maximalIdeal` `WithZero.one` `instOneMultiplicativeOfZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing`	`RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap`	—	`Multiplicative.isOrderedCancelMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `IsPrincipalIdealRing.isDedekindDomain` `toIsPrincipalIdealRing` `exists_irreducible` `IsFractionRing.div_surjective` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `zero_div` `eq_unit_mul_pow_irreducible` `nonZeroDivisors.ne_zero` `IsLocalRing.toNontrivial` `toIsLocalRing` `mul_mem_nonZeroDivisors` `IsScalarTower.right` `IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd` `dvd_of_eq` `irreducible_iff_uniformizer` `IsDedekindDomain.HeightOneSpectrum.intValuation_ne_zero` `Irreducible.ne_zero` `sub_nonneg` `covariant_swap_add_of_covariant_add` `Int.instAddLeftMono` `zpow_le_one_iff_right_of_lt_one₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `zero_lt_iff` `sub_eq_add_neg` `zpow_add₀` `zpow_neg` `ofAdd_zero` `zpow_natCast` `div_eq_mul_inv` `WithZero.coe_one` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `IsDedekindDomain.HeightOneSpectrum.valuation_of_mk'` `IsFractionRing.mk'_mk_eq_div` `map_div₀` `mul_one` `inv_one` `Multiplicative.isOrderedMonoid` `Int.instIsOrderedAddMonoid` `Valuation.Integers.one_of_isUnit'` `Units.isUnit` `IsDedekindDomain.HeightOneSpectrum.valuation_le_one` `map_inv₀` `map_mul` `MonoidHomClass.toMulHomClass` `Valuation.map_mul` `mul_assoc` `mul_inv` `one_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `mul_comm` `map_units_inv` `mul_div_assoc` `pow_sub₀` `IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors` `mem_nonZeroDivisors_iff_ne_zero` `IsDomain.to_noZeroDivisors`
`isRankOneDiscrete` 📖	mathematical	—	`Valuation.IsRankOneDiscrete` `WithZero` `Multiplicative` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `Multiplicative.isOrderedMonoid` `Int.instAddCommMonoid` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Int.instIsOrderedAddMonoid` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `IsPrincipalIdealRing.isDedekindDomain` `toIsPrincipalIdealRing` `maximalIdeal`	—	`Multiplicative.isOrderedCancelMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `IsPrincipalIdealRing.isDedekindDomain` `toIsPrincipalIdealRing` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer` `Subgroup.nontrivial_iff_exists_ne_one` `MonoidWithZeroHom.mem_valueGroup` `instLawfulBCmpCompare_mathlib` `Multiplicative.isOrderedMonoid` `Int.instIsOrderedAddMonoid` `Valuation.IsRankOneDiscrete.mk'` `Subgroup.isCyclic` `instIsCyclicUnitsWithZero` `isCyclic_multiplicative` `instIsAddCyclicInt`
`map_algebraMap_eq_valuationSubring` 📖	mathematical	—	`Subring.map` `CommRing.toRing` `DivisionRing.toRing` `Field.toDivisionRing` `algebraMap` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Top.top` `Subring` `Subring.instTop` `ValuationSubring.toSubring` `Valuation.valuationSubring` `WithZero` `Multiplicative` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `Multiplicative.isOrderedMonoid` `Int.instAddCommMonoid` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Int.instIsOrderedAddMonoid` `IsDedekindDomain.HeightOneSpectrum.valuation` `IsPrincipalIdealRing.isDedekindDomain` `toIsPrincipalIdealRing` `maximalIdeal`	—	`Subring.ext` `Multiplicative.isOrderedMonoid` `Int.instIsOrderedAddMonoid` `IsPrincipalIdealRing.isDedekindDomain` `toIsPrincipalIdealRing` `Subring.mem_map` `IsDedekindDomain.HeightOneSpectrum.valuation_le_one` `exists_lift_of_le_one` `Subring.mem_top`

Valuation

Definitions

Name	Category	Theorems
`IsRankOneDiscrete` 📖	CompData	2 math math: `IsDiscreteValuationRing.isRankOneDiscrete`, `IsRankOneDiscrete.mk'`
`IsUniformizer` 📖	MathDef	4 math math: `exists_isUniformizer_of_isCyclic_of_nontrivial`, `IsUniformizer.iff`, `isUniformizer_of_maximalIdeal_eq_span`, `Uniformizer.valuation_gt_one`
`Uniformizer` 📖	CompData	1 math math: `instNonemptyUniformizer`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`associated_of_isUniformizer` 📖	mathematical	`IsUniformizer` `DivisionRing.toRing` `Field.toDivisionRing` `ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `valuationSubring`	`Associated` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `ValuationSubring.instSubringClass`	—	`map_mul` `MonoidHomClass.toMulHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `ValuationClass.toMonoidWithZeroHomClass` `instValuationClass` `map_inv₀` `IsUniformizer.iff` `inv_mul_cancel₀` `GroupWithZero.toNontrivial` `mem_integer_iff` `le_of_eq` `SubringClass.toSubsemiringClass` `ValuationSubring.instSubringClass` `Integers.isUnit_iff_valuation_eq_one` `integer.integers` `Subtype.val_injective` `IsUnit.unit.congr_simp` `mul_inv_cancel₀` `IsUniformizer.ne_zero` `one_mul`
`exists_isUniformizer_of_isCyclic_of_nontrivial` 📖	mathematical	—	`IsUniformizer` `DivisionRing.toRing` `Field.toDivisionRing` `IsRankOneDiscrete.mk'` `ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `valuationSubring`	—	`ValuationClass.toMonoidWithZeroHomClass` `instValuationClass` `IsRankOneDiscrete.mk'` `Units.isOrderedMonoid` `LinearOrderedCommMonoidWithZero.toIsOrderedMonoid` `MonoidWithZeroHom.valueGroup_eq_range` `Set.mem_image_of_mem` `LinearOrderedCommGroup.Subgroup.genLTOne_mem` `le_of_lt` `LinearOrderedCommGroup.Subgroup.genLTOne_lt_one` `instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial` `IsRankOneDiscrete.instIsNontrivial` `IsRankOneDiscrete.instIsCyclicSubtypeUnitsMemSubgroupValueGroup` `IsRankOneDiscrete.valueGroup_genLTOne_eq_generator`
`exists_pow_Uniformizer` 📖	mathematical	—	`ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `valuationSubring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Subring` `DivisionRing.toRing` `Field.toDivisionRing` `Subring.instSetLike` `integer` `SubmonoidClass.nPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SubsemiringClass.toSubmonoidClass` `Semiring.toNonAssocSemiring` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `Uniformizer.val` `Units.val` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `ValuationSubring.instSubringClass`	—	`AddSubmonoidClass.toZeroMemClass` `SubsemiringClass.toAddSubmonoidClass` `SubringClass.toSubsemiringClass` `ValuationSubring.instSubringClass` `zero_iff` `GroupWithZero.toNontrivial` `AddSubgroupClass.toAddSubmonoidClass` `SubringClass.addSubgroupClass` `Subring.instSubringClass` `Subring.coe_eq_zero_iff` `ValuationClass.toMonoidWithZeroHomClass` `instValuationClass` `MonoidWithZeroHom.mem_valueGroup` `Units.val_mk0` `Set.mem_range_self` `IsUniformizer.val_ne_zero` `Uniformizer.valuation_gt_one` `SubsemiringClass.toSubmonoidClass` `Subgroup.mem_zpowers_iff` `IsUniformizer.zpowers_eq_valueGroup` `Units.val_zpow_eq_zpow_val` `zpow_le_one_iff_right_of_lt_one₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `IsUniformizer.val_pos` `IsUniformizer.val_lt_one` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `map_zpow₀` `zpow_neg` `inv_mul_cancel₀` `le_of_eq` `IsDomain.to_noZeroDivisors` `instIsDomain` `zpow_natCast` `pow_eq_zero_iff'` `isReduced_of_noZeroDivisors` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `not_and_or` `Uniformizer.ne_zero` `Integers.isUnit_of_one` `integer.integers` `isUnit_iff_ne_zero` `IsUnit.unit_spec` `Subring.coe_pow` `mul_assoc` `mul_inv_cancel₀` `pow_ne_zero` `one_mul`
`ideal_isPrincipal` 📖	mathematical	—	`Submodule.IsPrincipal` `ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `valuationSubring` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `DivisionRing.toRing` `Field.toDivisionRing` `ValuationSubring.instSubringClass` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`ValuationClass.toMonoidWithZeroHomClass` `instValuationClass` `SubringClass.toSubsemiringClass` `ValuationSubring.instSubringClass` `ValuationRing.toPreValuationRing` `ValuationSubring.instIsDomainSubtypeMem` `ValuationSubring.instValuationRingSubtypeMem` `bot_isPrincipal` `IsRankOneDiscrete.mk'` `instNonemptyUniformizer` `Submodule.exists_mem_ne_zero_of_ne_bot` `SubsemiringClass.toSubmonoidClass` `Subring.instSubringClass` `exists_pow_Uniformizer` `Ideal.IsPrime.ne_top` `Ideal.eq_top_of_isUnit_mem` `SetLike.coe_eq_coe` `one_mul` `pow_zero` `Subring.coe_mul` `ValuationSubring.isLocalRing` `Ideal.IsMaximal.eq_of_le` `IsLocalRing.maximalIdeal.isMaximal` `Uniformizer.is_generator` `Ideal.span_singleton_le_iff_mem` `Ideal.IsPrime.pow_mem_iff_mem` `pos_iff_ne_zero` `Nat.instCanonicallyOrderedAdd` `Ideal.mul_unit_mem_iff_mem` `Units.isUnit` `IsPrincipalIdealRing.principal` `IsPrincipalIdealRing.of_prime`
`instNonemptyUniformizer` 📖	mathematical	—	`Uniformizer` `DivisionRing.toRing` `Field.toDivisionRing` `IsRankOneDiscrete.mk'`	—	`ValuationClass.toMonoidWithZeroHomClass` `instValuationClass` `IsRankOneDiscrete.mk'` `exists_isUniformizer_of_isCyclic_of_nontrivial`
`isUniformizer_of_maximalIdeal_eq_span` 📖	mathematical	`IsLocalRing.maximalIdeal` `ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `valuationSubring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `DivisionRing.toRing` `Field.toDivisionRing` `ValuationSubring.instSubringClass` `ValuationSubring.isLocalRing` `Ideal.span` `CommSemiring.toSemiring` `Set` `Set.instSingletonSet`	`IsUniformizer`	—	`SubringClass.toSubsemiringClass` `ValuationSubring.instSubringClass` `ValuationSubring.isLocalRing` `AddSubmonoidClass.toZeroMemClass` `SubsemiringClass.toAddSubmonoidClass` `Ring.ne_bot_of_isMaximal_of_not_isField` `SubsemiringClass.nontrivial` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsLocalRing.maximalIdeal.isMaximal` `valuationSubring_not_isField` `instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial` `IsRankOneDiscrete.instIsNontrivial` `IsRankOneDiscrete.instIsCyclicSubtypeUnitsMemSubgroupValueGroup` `Ideal.span_zero` `Set.singleton_zero` `IsRankOneDiscrete.mk'` `exists_isUniformizer_of_isCyclic_of_nontrivial` `SubsemiringClass.toSubmonoidClass` `Subring.instSubringClass` `exists_pow_Uniformizer` `IsUniformizer.of_associated` `Ideal.span_singleton_eq_span_singleton` `Subring.instIsDomainSubtypeMem` `instIsDomain` `Uniformizer.is_generator`
`pow_Uniformizer_is_pow_generator` 📖	mathematical	—	`Ideal` `ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `valuationSubring` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `DivisionRing.toRing` `Field.toDivisionRing` `ValuationSubring.instSubringClass` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `IsLocalRing.maximalIdeal` `ValuationSubring.isLocalRing` `Ideal.span` `Subring` `Subring.instSetLike` `integer` `Subring.instSubringClass` `Set` `Set.instSingletonSet` `SubmonoidClass.nPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `SubsemiringClass.toSubmonoidClass` `Semiring.toNonAssocSemiring` `Uniformizer.val`	—	`SubringClass.toSubsemiringClass` `ValuationSubring.instSubringClass` `IsScalarTower.right` `ValuationSubring.isLocalRing` `Subring.instSubringClass` `SubsemiringClass.toSubmonoidClass` `IsScalarTower.left` `Ideal.span_singleton_pow` `Ideal.instIsTwoSided_1` `Uniformizer.is_generator`
`valuationSubring_isDiscreteValuationRing` 📖	mathematical	—	`IsDiscreteValuationRing` `ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `valuationSubring` `ValuationSubring.instCommRingSubtypeMem` `ValuationSubring.instIsDomainSubtypeMem`	—	`ValuationClass.toMonoidWithZeroHomClass` `instValuationClass` `valuationSubring_isPrincipalIdealRing` `ValuationSubring.isLocalRing` `ValuationSubring.instIsDomainSubtypeMem` `IsLocalRing.isField_iff_maximalIdeal_eq` `valuationSubring_not_isField`
`valuationSubring_isPrincipalIdealRing` 📖	mathematical	—	`IsPrincipalIdealRing` `ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `valuationSubring` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `DivisionRing.toRing` `Field.toDivisionRing` `ValuationSubring.instSubringClass`	—	`ValuationClass.toMonoidWithZeroHomClass` `instValuationClass` `SubringClass.toSubsemiringClass` `ValuationSubring.instSubringClass` `ideal_isPrincipal`
`valuationSubring_not_isField` 📖	mathematical	—	`IsField` `ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `valuationSubring` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `DivisionRing.toRing` `Field.toDivisionRing` `ValuationSubring.instSubringClass`	—	`ValuationClass.toMonoidWithZeroHomClass` `instValuationClass` `IsRankOneDiscrete.mk'` `SubringClass.toSubsemiringClass` `ValuationSubring.instSubringClass` `exists_isUniformizer_of_isCyclic_of_nontrivial` `IsUniformizer.ne_zero` `IsUniformizer.not_isUnit` `isUnit_iff_exists_inv` `SubmonoidClass.instIsDedekindFiniteMonoidSubtypeMem` `SubsemiringClass.toSubmonoidClass` `instIsDedekindFiniteMonoid` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `SubringClass.addSubgroupClass` `Subring.instSubringClass`

Valuation.IsRankOneDiscrete

Definitions

Name	Category	Theorems
`generator` 📖	CompOp	8 math math: `generator_lt_one`, `generator_mem_valueGroup`, `Valuation.IsUniformizer.val`, `valueGroup_genLTOne_eq_generator`, `generator_zpowers_eq_range`, `generator_zpowers_eq_valueGroup`, `Valuation.IsUniformizer.iff`, `generator_mem_range`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_generator_lt_one` 📖	mathematical	—	`Subgroup.zpowers` `Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `Units.instGroup` `MonoidWithZeroHom.valueGroup` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `Valuation.instFunLike` `Semiring.toMonoidWithZero` `Ring.toSemiring` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `Preorder.toLT` `Units.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `Units.instOne`	—	`exists_generator_lt_one'`
`exists_generator_lt_one'` 📖	mathematical	—	`Subgroup.zpowers` `Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `Units.instGroup` `MonoidWithZeroHom.valueGroup` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `Valuation.instFunLike` `Semiring.toMonoidWithZero` `Ring.toSemiring` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `Preorder.toLT` `Units.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `Units.instOne`	—	—
`generator_lt_one` 📖	mathematical	—	`Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `Preorder.toLT` `Units.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `generator` `Units.instOne`	—	`ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `exists_generator_lt_one`
`generator_mem_range` 📖	mathematical	—	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DivisionRing.toRing` `Field.toDivisionRing` `Valuation.instFunLike` `Units.val` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `generator`	—	`Set.diff_subset` `generator_zpowers_eq_range`
`generator_mem_valueGroup` 📖	mathematical	—	`Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidWithZeroHom.valueGroup` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `Valuation.instFunLike` `Semiring.toMonoidWithZero` `Ring.toSemiring` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `generator`	—	`ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `generator_zpowers_eq_valueGroup` `Subgroup.mem_zpowers`
`generator_ne_one` 📖	—	—	—	—	`ne_of_lt` `generator_lt_one`
`generator_ne_zero` 📖	—	—	—	—	`GroupWithZero.toNontrivial`
`generator_zpowers_eq_range` 📖	mathematical	—	`Set.image` `Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `Units.val` `SetLike.coe` `Subgroup` `Units.instGroup` `Subgroup.instSetLike` `Subgroup.zpowers` `generator` `DivisionRing.toRing` `Field.toDivisionRing` `Set` `Set.instSDiff` `Set.range` `DFunLike.coe` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `Valuation.instFunLike` `Set.instSingletonSet` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	`ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `generator_zpowers_eq_valueGroup` `MonoidWithZeroHom.valueGroup_eq_range`
`generator_zpowers_eq_valueGroup` 📖	mathematical	—	`Subgroup.zpowers` `Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `Units.instGroup` `generator` `MonoidWithZeroHom.valueGroup` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `Valuation.instFunLike` `Semiring.toMonoidWithZero` `Ring.toSemiring` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass`	—	`ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `exists_generator_lt_one`
`instIsCyclicSubtypeUnitsMemSubgroupValueGroup` 📖	mathematical	—	`IsCyclic` `Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidWithZeroHom.valueGroup` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `Valuation.instFunLike` `Semiring.toMonoidWithZero` `Ring.toSemiring` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `Subgroup.zpow`	—	`ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `generator_zpowers_eq_valueGroup` `Subgroup.isCyclic_zpowers`
`instIsNontrivial` 📖	mathematical	—	`Valuation.IsNontrivial` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero`	—	`ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Push.not_and_eq` `generator_lt_one` `generator_zpowers_eq_valueGroup`
`mk'` 📖	mathematical	—	`Valuation.IsRankOneDiscrete`	—	`ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `Units.isOrderedMonoid` `LinearOrderedCommMonoidWithZero.toIsOrderedMonoid` `LinearOrderedCommGroup.Subgroup.genLTOne_zpowers_eq_top` `LinearOrderedCommGroup.Subgroup.genLTOne_lt_one`
`valueGroup_genLTOne_eq_generator` 📖	mathematical	—	`LinearOrderedCommGroup.Subgroup.genLTOne` `Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `Units.instCommGroupUnits` `CommMonoidWithZero.toCommMonoid` `LinearOrderedCommMonoidWithZero.toCommMonoidWithZero` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `Units.instLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `Units.isOrderedMonoid` `LinearOrder.toPartialOrder` `LinearOrderedCommMonoidWithZero.toIsOrderedMonoid` `MonoidWithZeroHom.valueGroup` `Valuation` `Valuation.instFunLike` `Semiring.toMonoidWithZero` `Ring.toSemiring` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `Valuation.instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial` `instIsNontrivial` `instIsCyclicSubtypeUnitsMemSubgroupValueGroup` `generator`	—	`Units.isOrderedMonoid` `LinearOrderedCommMonoidWithZero.toIsOrderedMonoid` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `Valuation.instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial` `instIsNontrivial` `instIsCyclicSubtypeUnitsMemSubgroupValueGroup` `LinearOrderedCommGroup.Subgroup.genLTOne_unique` `generator_lt_one` `generator_zpowers_eq_valueGroup`

Valuation.IsUniformizer

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iff` 📖	mathematical	—	`Valuation.IsUniformizer` `DFunLike.coe` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `Valuation.instFunLike` `Units.val` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `Valuation.IsRankOneDiscrete.generator`	—	`refl` `IsPreorder.toRefl` `IsEquiv.toIsPreorder` `iff_isEquiv`
`is_generator` 📖	mathematical	`Valuation.IsUniformizer` `DivisionRing.toRing` `Field.toDivisionRing` `ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `Valuation.valuationSubring`	`IsLocalRing.maximalIdeal` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `ValuationSubring.instSubringClass` `ValuationSubring.isLocalRing` `Ideal.span` `CommSemiring.toSemiring` `Set` `Set.instSingletonSet`	—	`Valuation.Uniformizer.is_generator`
`ne_zero` 📖	—	`Valuation.IsUniformizer`	—	—	`Units.ne_zero` `GroupWithZero.toNontrivial` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `eq_1`
`not_isUnit` 📖	mathematical	`Valuation.IsUniformizer` `CommRing.toRing` `Subring` `SetLike.instMembership` `Subring.instSetLike` `Valuation.integer`	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `CommRing.toCommSemiring` `SubringClass.toSubsemiringClass` `Subring.instSubringClass`	—	`SubringClass.toSubsemiringClass` `Subring.instSubringClass` `ne_of_gt` `val_lt_one` `Valuation.Integers.one_of_isUnit` `Valuation.integer.integers`
`of_associated` 📖	—	`Valuation.IsUniformizer` `DivisionRing.toRing` `Field.toDivisionRing` `ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `Valuation.valuationSubring` `Associated` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `ValuationSubring.instSubringClass`	—	—	`SubringClass.toSubsemiringClass` `ValuationSubring.instSubringClass` `Valuation.Integers.isUnit_iff_valuation_eq_one` `Valuation.integer.integers` `Units.isUnit` `iff` `Subring.coe_mul` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `mul_one`
`val` 📖	mathematical	`Valuation.IsUniformizer`	`DFunLike.coe` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `Valuation.instFunLike` `Units.val` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `Valuation.IsRankOneDiscrete.generator`	—	—
`val_lt_one` 📖	mathematical	`Valuation.IsUniformizer`	`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`	—	`Valuation.IsRankOneDiscrete.generator_lt_one`
`val_ne_zero` 📖	—	`Valuation.IsUniformizer`	—	—	`Units.ne_zero` `GroupWithZero.toNontrivial`
`val_pos` 📖	mathematical	`Valuation.IsUniformizer`	`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`	—	`iff` `GroupWithZero.toNontrivial`
`zpowers_eq_valueGroup` 📖	mathematical	`Valuation.IsUniformizer`	`MonoidWithZeroHom.valueGroup` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `Valuation.instFunLike` `Semiring.toMonoidWithZero` `Ring.toSemiring` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `Subgroup.zpowers` `Units` `MonoidWithZero.toMonoid` `Units.instGroup` `DFunLike.coe` `val_ne_zero`	—	`ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `val_ne_zero` `Units.isOrderedMonoid` `LinearOrderedCommMonoidWithZero.toIsOrderedMonoid` `Valuation.instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial` `Valuation.IsRankOneDiscrete.instIsNontrivial` `Valuation.IsRankOneDiscrete.instIsCyclicSubtypeUnitsMemSubgroupValueGroup` `LinearOrderedCommGroup.Subgroup.genLTOne_zpowers_eq_top` `val` `Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator`

Valuation.Uniformizer

Definitions

Name	Category	Theorems
`instCoeSubtypeMemSubringInteger` 📖	CompOp	—
`mk'` 📖	CompOp	—
`val` 📖	CompOp	5 math math: `ext_iff`, `Valuation.pow_Uniformizer_is_pow_generator`, `Valuation.exists_pow_Uniformizer`, `is_generator`, `valuation_gt_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`val`	—	—	—
`ext_iff` 📖	mathematical	—	`val`	—	`ext`
`is_generator` 📖	mathematical	—	`IsLocalRing.maximalIdeal` `ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `Valuation.valuationSubring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `DivisionRing.toRing` `Field.toDivisionRing` `ValuationSubring.instSubringClass` `ValuationSubring.isLocalRing` `Ideal.span` `Subring` `Subring.instSetLike` `Valuation.integer` `CommSemiring.toSemiring` `Subring.instSubringClass` `Set` `Set.instSingletonSet` `val`	—	`Ideal.IsMaximal.eq_of_le` `SubringClass.toSubsemiringClass` `ValuationSubring.instSubringClass` `ValuationSubring.isLocalRing` `Subring.instSubringClass` `IsLocalRing.maximalIdeal.isMaximal` `Valuation.IsUniformizer.not_isUnit` `valuation_gt_one` `Ideal.span_singleton_eq_top` `AddSubmonoidClass.toZeroMemClass` `SubsemiringClass.toAddSubmonoidClass` `Submodule.addSubmonoidClass` `SubsemiringClass.toSubmonoidClass` `Valuation.exists_pow_Uniformizer` `Ideal.IsMaximal.ne_top` `Ideal.eq_top_of_isUnit_mem` `Subring.coe_mul` `pow_zero` `one_mul` `dvd_pow_self`
`ne_zero` 📖	—	—	—	—	`Valuation.IsUniformizer.ne_zero` `valuation_gt_one`
`valuation_gt_one` 📖	mathematical	—	`Valuation.IsUniformizer` `Subring` `SetLike.instMembership` `Subring.instSetLike` `Valuation.integer` `val`	—	—

---

← Back to Index