Factorial

Statistics

Metric	Count
Definitions	0
Theorems `cast_descFactorial`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_descFactorial` 📖	mathematical	—	`ZMod` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `commRing` `Nat.descFactorial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `Nat.factorial`	—	`Nat.descFactorial_eq_prod_range` `Nat.factorial_eq_prod_range_add_one` `Nat.cast_prod` `Finset.card_range` `Finset.pow_card_mul_prod` `Finset.prod_congr` `tsub_add_eq_tsub_tsub_swap` `Nat.instOrderedSub` `Nat.cast_sub` `CharP.cast_eq_zero` `charP` `zero_sub` `Nat.cast_succ` `neg_add_rev` `mul_add` `Distrib.leftDistribClass` `neg_mul` `one_mul` `mul_one` `add_comm`

---