Cast

Statistics

Metric	Count
Definitions	0
Theorems `cast_descFactorial_two`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_descFactorial_two` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `descFactorial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddMonoidWithOne.toOne`	—	`descFactorial.eq_2` `mul_one` `MulZeroClass.mul_zero` `cast_zero` `zero_sub` `mul_neg` `neg_zero` `mul_add` `Distrib.leftDistribClass` `cast_add` `cast_mul` `cast_one` `add_sub_cancel_right` `add_mul` `Distrib.rightDistribClass` `one_mul`

---