Documentation Verification Report

ValuativeRel

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

Statistics

MetricCount
DefinitionsinstValuativeRel
1
TheoremsinstCompatibleWithZeroMultiplicativeIntMulValuation, instIsNontrivial, instIsRankLeOne, valuation_p_lt_one, valuation_p_ne_zero
5
Total6

Padic

Definitions

NameCategoryTheorems
instValuativeRel 📖CompOp
3 mathmath: instCompatibleWithZeroMultiplicativeIntMulValuation, instIsRankLeOne, instIsNontrivial

Theorems

NameKindAssumesProvesValidatesDepends On
instCompatibleWithZeroMultiplicativeIntMulValuation 📖mathematicalValuation.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 📖mathematicalValuativeRel.IsNontrivial
Padic
instCommRing
instValuativeRel
valuation_p_ne_zero
ValuativeRel.instCompatibleValueGroupWithZeroValuation
LT.lt.ne
valuation_p_lt_one
instIsRankLeOne 📖mathematicalValuativeRel.IsRankLeOne
Padic
instCommRing
instValuativeRel
ValuativeRel.IsRankLeOne.of_compatible_mulArchimedean
Multiplicative.isOrderedMonoid
Int.instIsOrderedAddMonoid
WithZero.instMulArchimedean
Multiplicative.instMulArchimedean
instArchimedeanInt
instCompatibleWithZeroMultiplicativeIntMulValuation
valuation_p_lt_one 📖mathematicalPreorder.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