Field

Statistics

Metric	Count
Definitions	0
Theorems `cast_div`, `cast_div_charZero`, `cast_div_div_div_cancel_right`	3
Total	3

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_div` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero`	—	`cast_zero` `mul_comm` `cast_mul` `mul_div_cancel_right₀` `GroupWithZero.toMulDivCancelClass`
`cast_div_charZero` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero`	—	`eq_or_ne` `cast_zero` `div_zero` `cast_div`
`cast_div_div_div_cancel_right` 📖	mathematical	—	`DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring`	—	`eq_or_ne` `cast_zero` `div_zero` `zero_div` `cast_div` `div_div_div_cancel_right₀`

---