Field

Statistics

Metric	Count
Definitions	0
Theorems `cast_div`, `cast_neg_natCast`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_div` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid`	—	`cast_zero` `mul_comm` `cast_mul` `mul_div_cancel_right₀` `GroupWithZero.toMulDivCancelClass`
`cast_neg_natCast` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne`	—	`cast_neg` `cast_natCast`

---