FactorialInv

📁 Source: SDG/Basic/FactorialInv.lean

Statistics

Metric	Count
Definitions Divisible, divisible, instInvertibleCastFactorial_sDG	3
Theorems inv_factorial_one, inv_factorial_zero, succ_mul_inv_factorial_succ	3
Total	6

SDG

Definitions

Name	Category	Theorems
Divisible 📖	CompData	—
instInvertibleCastFactorial_sDG 📖	CompOp	5 math math: succ_mul_inv_factorial_succ, inv_factorial_one, inv_factorial_zero, taylor_k_aux, taylor_k

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inv_factorial_one 📖	mathematical	—	instInvertibleCastFactorial_sDG	—	—
inv_factorial_zero 📖	mathematical	—	instInvertibleCastFactorial_sDG	—	—
succ_mul_inv_factorial_succ 📖	mathematical	—	instInvertibleCastFactorial_sDG	—	—

SDG.Divisible

Definitions

Name	Category	Theorems
divisible 📖	CompOp	—

---

← Back to Index