Documentation Verification Report

Ostrowski

📁 Source: Mathlib/NumberTheory/RatFunc/Ostrowski.lean

Statistics

Metric	Count
Definitions `uniformizingPolynomial`, `valuationIdeal`	2
Theorems `adicValuation_ne_inftyValuation`, `adicValuation_not_isEquiv_infty_valuation`, `exists_zpow_uniformizingPolynomial`, `irreducible_min_polynomial_valuation_lt_one_and_ne_zero`, `setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty`, `uniformizingPolynomial_isUniformizer`, `uniformizingPolynomial_ne_zero`, `valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X`, `valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one`, `valuation_isEquiv_adic_of_not_isEquiv_infty`, `valuation_isEquiv_adic_of_valuation_X_le_one`, `valuation_isEquiv_inftyValuation_of_one_lt_valuation_X`, `valuation_isEquiv_infty_or_adic`, `valuation_isEquiv_valuationIdeal_adic_of_valuation_X_le_one`, `valuation_uniformizingPolynomial_lt_one`	15
Total	17

RatFunc

Definitions

Name	Category	Theorems
`uniformizingPolynomial` 📖	CompOp	4 math math: `exists_zpow_uniformizingPolynomial`, `valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one`, `valuation_uniformizingPolynomial_lt_one`, `uniformizingPolynomial_isUniformizer`
`valuationIdeal` 📖	CompOp	2 math math: `valuation_isEquiv_valuationIdeal_adic_of_valuation_X_le_one`, `valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adicValuation_ne_inftyValuation` 📖	—	—	—	—	`Multiplicative.isOrderedCancelMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `instIsDomain` `IsPrincipalIdealRing.isDedekindDomain` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `EuclideanDomain.to_principal_ideal_domain` `instIsFractionRingPolynomial` `Valuation.IsEquiv.refl` `adicValuation_not_isEquiv_infty_valuation`
`adicValuation_not_isEquiv_infty_valuation` 📖	mathematical	—	`Valuation.IsEquiv` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `WithZero` `Multiplicative` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instIsDomain` `Field.toSemifield` `WithZero.instLinearOrderedCommMonoidWithZero` `Multiplicative.commMonoid` `Int.instAddCommMonoid` `Multiplicative.linearOrder` `Int.instLinearOrder` `Multiplicative.isOrderedCancelMonoid` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `instLatticeInt` `Int.instIsStrictOrderedRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Polynomial.commRing` `IsPrincipalIdealRing.isDedekindDomain` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `AddGroup.toAddCancelMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `EuclideanDomain.to_principal_ideal_domain` `Polynomial.instEuclideanDomain` `instAlgebraOfPolynomial` `CommRing.toCommSemiring` `Algebra.id` `instIsFractionRingPolynomial` `FunctionField.inftyValuation`	—	`instIsDomain` `Multiplicative.isOrderedCancelMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `IsPrincipalIdealRing.isDedekindDomain` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `EuclideanDomain.to_principal_ideal_domain` `instIsFractionRingPolynomial` `Multiplicative.isOrderedMonoid` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Push.not_forall_eq` `IsDedekindDomain.HeightOneSpectrum.valuation_le_one` `FunctionField.inftyValuation.X` `WithZero.log_lt_iff_lt_exp` `one_ne_zero` `NeZero.one` `WithZero.instNontrivial` `WithZero.log_one` `zero_lt_one` `Int.instZeroLEOneClass`
`exists_zpow_uniformizingPolynomial` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DFunLike.coe` `Valuation` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instIsDomain` `Field.toSemifield` `Valuation.instFunLike` `X` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `LinearOrderedCommGroupWithZero.toCommGroupWithZero`	`DFunLike.coe` `Valuation` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instIsDomain` `Field.toSemifield` `Valuation.instFunLike` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `coePolynomial` `uniformizingPolynomial`	—	`instIsDomain` `GroupWithZero.toNontrivial` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `Module.IsTorsionFree.to_faithfulSMul` `Polynomial.instIsCancelMulZeroOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `IsDomain.toIsCancelMulZero` `instNontrivial` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `FaithfulSMul.to_isTorsionFree` `IsFractionRing.instFaithfulSMul` `instIsFractionRingPolynomial` `Polynomial.nontrivial` `uniformizingPolynomial_ne_zero` `induction_on` `Ideal.uniqueFactorizationMonoid` `IsPrincipalIdealRing.isDedekindDomain` `Polynomial.instIsDomainOfIsCancelAdd` `EuclideanDomain.to_principal_ideal_domain` `map_div₀` `valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `zpow_sub₀` `zpow_natCast`
`irreducible_min_polynomial_valuation_lt_one_and_ne_zero` 📖	mathematical	`Set.Nonempty` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DFunLike.coe` `Valuation` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instIsDomain` `Valuation.instFunLike` `coePolynomial` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `Polynomial.instZero`	`Irreducible` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `WellFounded.min` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `Polynomial.degree_lt_wf` `setOf` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DFunLike.coe` `Valuation` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instIsDomain` `Valuation.instFunLike` `coePolynomial` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `Polynomial.instZero`	—	`instIsDomain` `Polynomial.degree_lt_wf` `WellFounded.min_mem` `irreducible_iff` `IsDomain.to_noZeroDivisors` `algebraMap_eq_C` `algebraMap_C` `coePolynomial.eq_1` `coePolynomial.congr_simp` `Polynomial.instNoZeroDivisors` `Right.one_le_mul` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `LinearOrderedCommMonoidWithZero.toIsOrderedMonoid` `mul_comm` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `MonoidHomClass.toMulHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass`
`setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DFunLike.coe` `Valuation` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instIsDomain` `Field.toSemifield` `Valuation.instFunLike` `X` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `LinearOrderedCommGroupWithZero.toCommGroupWithZero`	`Set.Nonempty` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DFunLike.coe` `Valuation` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instIsDomain` `Valuation.instFunLike` `coePolynomial` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `Polynomial.instZero`	—	`instIsDomain` `Valuation.IsNontrivial.exists_lt_one` `induction_on` `not_and_or` `Module.IsTorsionFree.to_faithfulSMul` `Polynomial.instIsCancelMulZeroOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `IsDomain.toIsCancelMulZero` `instNontrivial` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `FaithfulSMul.to_isTorsionFree` `IsFractionRing.instFaithfulSMul` `instIsFractionRingPolynomial` `Polynomial.nontrivial` `inv_one` `one_div` `map_div₀` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `lt_iff_le_and_ne` `Polynomial.valuation_le_one_of_valuation_X_le_one`
`uniformizingPolynomial_isUniformizer` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DFunLike.coe` `Valuation` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instIsDomain` `Field.toSemifield` `Valuation.instFunLike` `X` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `LinearOrderedCommGroupWithZero.toCommGroupWithZero`	`Valuation.IsUniformizer` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instIsDomain` `Field.toSemifield` `coePolynomial` `uniformizingPolynomial`	—	`instIsDomain` `GroupWithZero.toNontrivial` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `Module.IsTorsionFree.to_faithfulSMul` `Polynomial.instIsCancelMulZeroOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `IsDomain.toIsCancelMulZero` `instNontrivial` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `FaithfulSMul.to_isTorsionFree` `IsFractionRing.instFaithfulSMul` `instIsFractionRingPolynomial` `Polynomial.nontrivial` `uniformizingPolynomial_ne_zero` `Valuation.IsUniformizer.eq_1` `Units.isOrderedMonoid` `LinearOrderedCommMonoidWithZero.toIsOrderedMonoid` `Valuation.instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial` `Valuation.IsRankOneDiscrete.instIsNontrivial` `Valuation.IsRankOneDiscrete.instIsCyclicSubtypeUnitsMemSubgroupValueGroup` `Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator` `Ne.isUnit` `IsUnit.unit_spec` `LinearOrderedCommGroup.Subgroup.genLTOne_unique` `Units.val_lt_val` `Units.val_one` `valuation_uniformizingPolynomial_lt_one` `Subgroup.ext` `one_ne_zero` `NeZero.one` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `Units.val_zpow_eq_zpow_val` `one_mul` `map_zpow₀` `exists_zpow_uniformizingPolynomial` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `GroupWithZero.noZeroDivisors` `zpow_ne_zero` `zpow_sub` `Units.val_inv_eq_inv_val` `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.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one`
`uniformizingPolynomial_ne_zero` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DFunLike.coe` `Valuation` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instIsDomain` `Field.toSemifield` `Valuation.instFunLike` `X` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `LinearOrderedCommGroupWithZero.toCommGroupWithZero`	—	—	`instIsDomain` `Polynomial.degree_lt_wf` `setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty` `WellFounded.min_mem`
`valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `DFunLike.coe` `Valuation` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instIsDomain` `Field.toSemifield` `Valuation.instFunLike` `X`	`DFunLike.coe` `Valuation` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instIsDomain` `Field.toSemifield` `Valuation.instFunLike` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `X` `intDegree`	—	`instIsDomain` `induction_on` `intDegree_div` `Valuation.map_div` `zpow_sub₀` `ne_zero_of_lt` `intDegree_polynomial` `zpow_natCast` `Mathlib.Tactic.Contrapose.contrapose₄` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `zero_div` `Polynomial.valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X`
`valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DFunLike.coe` `Valuation` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instIsDomain` `Field.toSemifield` `Valuation.instFunLike` `X` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `LinearOrderedCommGroupWithZero.toCommGroupWithZero`	`DFunLike.coe` `Valuation` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instIsDomain` `Field.toSemifield` `Valuation.instFunLike` `RingHom` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Polynomial.commSemiring` `Semifield.toCommSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebraOfPolynomial` `Algebra.id` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `coePolynomial` `uniformizingPolynomial` `Associates.count` `Ideal` `CommRing.toCommSemiring` `Polynomial.commRing` `CommSemiring.toCommMonoidWithZero` `IdemCommSemiring.toCommSemiring` `Ideal.instIdemCommSemiring` `Ideal.instDecidableEqAssociates` `Ideal.instDecidableIrreducibleAssociates` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Polynomial.semiring` `IsDedekindDomain.HeightOneSpectrum.asIdeal` `valuationIdeal` `Associates.factors` `Ideal.uniqueFactorizationMonoid` `IsPrincipalIdealRing.isDedekindDomain` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `AddGroup.toAddCancelMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `EuclideanDomain.to_principal_ideal_domain` `Polynomial.instEuclideanDomain` `Ideal.span` `Set` `Set.instSingletonSet`	—	`instIsDomain` `Ideal.uniqueFactorizationMonoid` `IsPrincipalIdealRing.isDedekindDomain` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `EuclideanDomain.to_principal_ideal_domain` `setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty` `irreducible_min_polynomial_valuation_lt_one_and_ne_zero` `WfDvdMonoid.max_power_factor` `UniqueFactorizationMonoid.toIsWellFounded` `Polynomial.uniqueFactorizationMonoid` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `WellFounded.min_mem` `Polynomial.degree_lt_wf` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `MonoidHomClass.toMulHomClass` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `EuclideanDomain.mod_add_div` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `coePolynomial_eq_algebraMap` `WellFounded.not_lt_min` `EuclideanDomain.remainder_lt` `Polynomial.valuation_le_one_of_valuation_X_le_one` `EuclideanDomain.mod_eq_zero` `mul_lt_one_of_lt_of_le` `IsOrderedMonoid.toMulLeftMono` `LinearOrderedCommMonoidWithZero.toIsOrderedMonoid` `Valuation.map_add_eq_of_lt_left` `mul_one` `Ideal.count_associates_eq` `irreducible_iff_prime` `Polynomial.instIsCancelMulZeroOfIsCancelAdd` `IsDomain.toIsCancelMulZero` `UniqueFactorizationMonoid.instDecompositionMonoid`
`valuation_isEquiv_adic_of_not_isEquiv_infty` 📖	mathematical	`Valuation.IsEquiv` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `WithZero` `Multiplicative` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instIsDomain` `Field.toSemifield` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `WithZero.instLinearOrderedCommMonoidWithZero` `Multiplicative.commMonoid` `Int.instAddCommMonoid` `Multiplicative.linearOrder` `Int.instLinearOrder` `Multiplicative.isOrderedCancelMonoid` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `instLatticeInt` `Int.instIsStrictOrderedRing` `FunctionField.inftyValuation`	`ExistsUnique` `IsDedekindDomain.HeightOneSpectrum` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.commRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Valuation.IsEquiv` `RatFunc` `WithZero` `Multiplicative` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instIsDomain` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `WithZero.instLinearOrderedCommMonoidWithZero` `Multiplicative.commMonoid` `Int.instAddCommMonoid` `Multiplicative.linearOrder` `Int.instLinearOrder` `Multiplicative.isOrderedCancelMonoid` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `instLatticeInt` `Int.instIsStrictOrderedRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `IsPrincipalIdealRing.isDedekindDomain` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `AddGroup.toAddCancelMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `EuclideanDomain.to_principal_ideal_domain` `Polynomial.instEuclideanDomain` `instAlgebraOfPolynomial` `CommRing.toCommSemiring` `Algebra.id` `instIsFractionRingPolynomial`	—	`instIsDomain` `Multiplicative.isOrderedCancelMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `IsPrincipalIdealRing.isDedekindDomain` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `EuclideanDomain.to_principal_ideal_domain` `instIsFractionRingPolynomial` `Xor'.or` `valuation_isEquiv_infty_or_adic`
`valuation_isEquiv_adic_of_valuation_X_le_one` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DFunLike.coe` `Valuation` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instIsDomain` `Field.toSemifield` `Valuation.instFunLike` `X` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `LinearOrderedCommGroupWithZero.toCommGroupWithZero`	`IsDedekindDomain.HeightOneSpectrum` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.commRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Valuation.IsEquiv` `RatFunc` `WithZero` `Multiplicative` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instIsDomain` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `WithZero.instLinearOrderedCommMonoidWithZero` `Multiplicative.commMonoid` `Int.instAddCommMonoid` `Multiplicative.linearOrder` `Int.instLinearOrder` `Multiplicative.isOrderedCancelMonoid` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `instLatticeInt` `Int.instIsStrictOrderedRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `IsPrincipalIdealRing.isDedekindDomain` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `AddGroup.toAddCancelMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `EuclideanDomain.to_principal_ideal_domain` `Polynomial.instEuclideanDomain` `instAlgebraOfPolynomial` `CommRing.toCommSemiring` `Algebra.id` `instIsFractionRingPolynomial`	—	`instIsDomain` `Multiplicative.isOrderedCancelMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `IsPrincipalIdealRing.isDedekindDomain` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `EuclideanDomain.to_principal_ideal_domain` `instIsFractionRingPolynomial` `Valuation.IsRankOneDiscrete.instIsNontrivial` `valuation_isEquiv_valuationIdeal_adic_of_valuation_X_le_one`
`valuation_isEquiv_inftyValuation_of_one_lt_valuation_X` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `DFunLike.coe` `Valuation` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instIsDomain` `Field.toSemifield` `Valuation.instFunLike` `X`	`Valuation.IsEquiv` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `WithZero` `Multiplicative` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instIsDomain` `Field.toSemifield` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `WithZero.instLinearOrderedCommMonoidWithZero` `Multiplicative.commMonoid` `Int.instAddCommMonoid` `Multiplicative.linearOrder` `Int.instLinearOrder` `Multiplicative.isOrderedCancelMonoid` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `instLatticeInt` `Int.instIsStrictOrderedRing` `FunctionField.inftyValuation`	—	`instIsDomain` `Multiplicative.isOrderedMonoid` `Int.instIsOrderedAddMonoid` `Valuation.isEquiv_iff_val_lt_one` `eq_or_ne` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `NeZero.one` `GroupWithZero.toNontrivial` `Multiplicative.isOrderedCancelMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `WithZero.instNontrivial` `FunctionField.inftyValuation.X` `Int.instZeroLEOneClass` `valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X` `FunctionField.instIsTrivialOnWithZeroMultiplicativeIntRatFuncInftyValuation`
`valuation_isEquiv_infty_or_adic` 📖	mathematical	—	`Xor'` `Valuation.IsEquiv` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `WithZero` `Multiplicative` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instIsDomain` `Field.toSemifield` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `WithZero.instLinearOrderedCommMonoidWithZero` `Multiplicative.commMonoid` `Int.instAddCommMonoid` `Multiplicative.linearOrder` `Int.instLinearOrder` `Multiplicative.isOrderedCancelMonoid` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `instLatticeInt` `Int.instIsStrictOrderedRing` `FunctionField.inftyValuation` `ExistsUnique` `IsDedekindDomain.HeightOneSpectrum` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Polynomial.commRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `IsPrincipalIdealRing.isDedekindDomain` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `AddGroup.toAddCancelMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `EuclideanDomain.to_principal_ideal_domain` `Polynomial.instEuclideanDomain` `instAlgebraOfPolynomial` `CommRing.toCommSemiring` `Algebra.id` `instIsFractionRingPolynomial`	—	`instIsDomain` `Multiplicative.isOrderedCancelMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `IsPrincipalIdealRing.isDedekindDomain` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `EuclideanDomain.to_principal_ideal_domain` `instIsFractionRingPolynomial` `lt_or_ge` `valuation_isEquiv_inftyValuation_of_one_lt_valuation_X` `Valuation.IsEquiv.trans` `Valuation.IsEquiv.symm` `adicValuation_not_isEquiv_infty_valuation` `valuation_isEquiv_adic_of_valuation_X_le_one` `IsDedekindDomain.HeightOneSpectrum.eq_of_valuation_isEquiv_valuation`
`valuation_isEquiv_valuationIdeal_adic_of_valuation_X_le_one` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DFunLike.coe` `Valuation` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instIsDomain` `Field.toSemifield` `Valuation.instFunLike` `X` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `LinearOrderedCommGroupWithZero.toCommGroupWithZero`	`Valuation.IsEquiv` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `WithZero` `Multiplicative` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instIsDomain` `Field.toSemifield` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `WithZero.instLinearOrderedCommMonoidWithZero` `Multiplicative.commMonoid` `Int.instAddCommMonoid` `Multiplicative.linearOrder` `Int.instLinearOrder` `Multiplicative.isOrderedCancelMonoid` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `instLatticeInt` `Int.instIsStrictOrderedRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Polynomial.commRing` `IsPrincipalIdealRing.isDedekindDomain` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `AddGroup.toAddCancelMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `EuclideanDomain.to_principal_ideal_domain` `Polynomial.instEuclideanDomain` `instAlgebraOfPolynomial` `CommRing.toCommSemiring` `Algebra.id` `instIsFractionRingPolynomial` `valuationIdeal`	—	`instIsDomain` `Multiplicative.isOrderedCancelMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `IsPrincipalIdealRing.isDedekindDomain` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `EuclideanDomain.to_principal_ideal_domain` `instIsFractionRingPolynomial` `Multiplicative.isOrderedMonoid` `Int.instIsOrderedAddMonoid` `Valuation.isEquiv_iff_val_le_one` `eq_or_ne` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `ValuationClass.toMonoidWithZeroHomClass` `Valuation.instValuationClass` `induction_on` `Module.IsTorsionFree.to_faithfulSMul` `Polynomial.instIsCancelMulZeroOfIsCancelAdd` `IsDomain.toIsCancelMulZero` `instNontrivial` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `FaithfulSMul.to_isTorsionFree` `IsFractionRing.instFaithfulSMul` `Polynomial.nontrivial` `uniformizingPolynomial_isUniformizer` `Ideal.uniqueFactorizationMonoid` `map_div₀` `IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap` `div_inv_eq_mul` `valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one` `Associates.count.congr_simp` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `Valuation.IsUniformizer.val` `Valuation.IsUniformizer.congr_simp` `coePolynomial.congr_simp` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `LinearOrderedCommMonoidWithZero.toMulPosStrictMono` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `pow_le_pow_iff_right_of_lt_one₀` `Valuation.IsRankOneDiscrete.generator_lt_one` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `instPosMulStrictMonoWithZeroOfMulLeftStrictMono` `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono` `Multiplicative.isLeftCancelMul` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsOrderedMonoid.toMulLeftMono` `Int.instAddLeftMono` `Int.instZeroLEOneClass` `Int.instCharZero`
`valuation_uniformizingPolynomial_lt_one` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DFunLike.coe` `Valuation` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instIsDomain` `Field.toSemifield` `Valuation.instFunLike` `X` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `LinearOrderedCommGroupWithZero.toCommGroupWithZero`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DFunLike.coe` `Valuation` `RatFunc` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instIsDomain` `Field.toSemifield` `Valuation.instFunLike` `coePolynomial` `uniformizingPolynomial` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `LinearOrderedCommGroupWithZero.toCommGroupWithZero`	—	`instIsDomain` `Polynomial.degree_lt_wf` `setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty` `WellFounded.min_mem`

---

← Back to Index