Field

Statistics

Metric	Count
Definitions	0
Theorems `coe_div`, `coe_inv`, `coe_ratCast`, `coe_zpow`	4
Total	4

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_div` 📖	mathematical	—	`Algebra.cast` `Semifield.toCommSemiring` `DivisionSemiring.toSemiring` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring`	—	`map_div₀` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`coe_inv` 📖	mathematical	—	`Algebra.cast` `Semifield.toCommSemiring` `DivisionSemiring.toSemiring` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero`	—	`map_inv₀` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`coe_ratCast` 📖	mathematical	—	`Algebra.cast` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `DivisionRing.toRatCast` `Field.toDivisionRing`	—	`map_ratCast` `RingHom.instRingHomClass`
`coe_zpow` 📖	mathematical	—	`Algebra.cast` `Semifield.toCommSemiring` `DivisionSemiring.toSemiring` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring`	—	`map_zpow₀` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`

---