FiniteField

Statistics

Metric	Count
Definitions	0
Theorems `algebraMap_eq_one`, `algebraMap_le_one`, `instIsTrivialOn`	3
Total	3

Name	Kind	Assumes	Proves	Validates	Depends On
`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`	—	`FiniteField.valuation_algebraMap_eq_one`
`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`	—	`FiniteField.valuation_algebraMap_le_one`
`instIsTrivialOn` 📖	mathematical	—	`Valuation.IsTrivialOn` `Semifield.toCommSemiring` `Field.toSemifield`	—	`FiniteField.instIsTrivialOn`

---