Valuation

📁 Source: Mathlib/FieldTheory/Finite/Valuation.lean

Statistics

Metric	Count
Definitions	0
Theorems instIsTrivialOn, valuation_algebraMap_eq_one, valuation_algebraMap_le_one	3
Total	3

FiniteField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsTrivialOn 📖	mathematical	—	Valuation.IsTrivialOn Semifield.toCommSemiring Field.toSemifield	—	valuation_algebraMap_eq_one
valuation_algebraMap_eq_one 📖	mathematical	—	DFunLike.coe Valuation Valuation.instFunLike RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield Ring.toSemiring RingHom.instFunLike algebraMap MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	—	MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass pow_card_sub_one_eq_one map_one MonoidHomClass.toOneHomClass
valuation_algebraMap_le_one 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder DFunLike.coe Valuation Valuation.instFunLike RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield Ring.toSemiring RingHom.instFunLike algebraMap MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero LinearOrderedCommMonoidWithZero.toCommMonoidWithZero	—	—

---

← Back to Index