Field

Statistics

Metric	Count
Definitions	0
Theorems `ringKrullDim_eq_zero_of_field`, `ringKrullDim_eq_zero_of_isField`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`ringKrullDim_eq_zero_of_field` 📖	mathematical	—	`ringKrullDim` `Semifield.toCommSemiring` `Field.toSemifield` `WithBot` `ENat` `WithBot.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`Order.krullDim_eq_zero_of_unique`
`ringKrullDim_eq_zero_of_isField` 📖	mathematical	`IsField` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`ringKrullDim` `CommRing.toCommSemiring` `WithBot` `ENat` `WithBot.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`Order.krullDim_eq_zero_of_unique`

---