ValuativeRel

📁 Source: Mathlib/NumberTheory/Padics/ValuativeRel.lean

Statistics

Metric	Count
Definitions instValuativeRel	1
Theorems instCompatibleWithZeroMultiplicativeIntMulValuation, instIsNontrivial, instIsRankLeOne, valuation_p_lt_one, valuation_p_ne_zero	5
Total	6

Padic

Definitions

Name	Category	Theorems
instValuativeRel 📖	CompOp	3 math math: instCompatibleWithZeroMultiplicativeIntMulValuation, instIsRankLeOne, instIsNontrivial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCompatibleWithZeroMultiplicativeIntMulValuation 📖	mathematical	—	Valuation.Compatible Padic WithZero Multiplicative instCommRing WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing mulValuation instValuativeRel	—	Valuation.Compatible.ofValuation Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid
instIsNontrivial 📖	mathematical	—	ValuativeRel.IsNontrivial Padic instCommRing instValuativeRel	—	valuation_p_ne_zero ValuativeRel.instCompatibleValueGroupWithZeroValuation LT.lt.ne valuation_p_lt_one
instIsRankLeOne 📖	mathematical	—	ValuativeRel.IsRankLeOne Padic instCommRing instValuativeRel	—	ValuativeRel.IsRankLeOne.of_compatible_mulArchimedean Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid WithZero.instMulArchimedean Multiplicative.instMulArchimedean instArchimedeanInt instCompatibleWithZeroMultiplicativeIntMulValuation
valuation_p_lt_one 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation Padic instRing Valuation.instFunLike AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Valuation.IsEquiv.lt_one_iff_lt_one ValuativeRel.isEquiv instCompatibleWithZeroMultiplicativeIntMulValuation instCharZero Nat.Prime.ne_zero Fact.out valuation_natCast padicValNat_self Nat.cast_one PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE instPosMulStrictMonoWithZeroOfMulLeftStrictMono IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono Multiplicative.isLeftCancelMul AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedMonoid.toMulLeftMono Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid NeZero.one WithZero.instNontrivial Int.instZeroLEOneClass
valuation_p_ne_zero 📖	—	—	—	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Valuation.IsEquiv.eq_zero ValuativeRel.isEquiv instCompatibleWithZeroMultiplicativeIntMulValuation instCharZero Nat.Prime.ne_zero Fact.out valuation_natCast padicValNat_self Nat.cast_one

---

← Back to Index