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`	—	`IsOfFinOrder.eq_one'` `LinearOrderedCommMonoidWithZero.toIsMulTorsionFree` `MonoidHom.isOfFinOrder` `IsUnit.isOfFinOrder` `instFiniteUnits` `Ne.isUnit`
`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`	—	—
`instIsTrivialOn` 📖	mathematical	—	`Valuation.IsTrivialOn` `Semifield.toCommSemiring` `Field.toSemifield`	—	`algebraMap_eq_one`

---