Taylor

📁 Source: SDG/IsKockLawvere/Taylor.lean

Statistics

Metric	Count
Definitions	0
Theorems taylor_k, taylor_k_aux, taylor_k_aux', taylor_k_aux_zero, taylor_two	5
Total	5

SDG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
taylor_k 📖	mathematical	—	𝔻 List.Fin.fintype instFunLikeDerivationForall_sDG deriv instIsKockLawvere_oneOfIsKockLawvere instInvertibleCastFactorial_sDG	—	instIsKockLawvere_oneOfIsKockLawvere inv_factorial_zero IsKockLawvere.isKockLawvere Fin.sum_univ_succ taylor_k_aux'
taylor_k_aux 📖	mathematical	—	List.Fin.fintype D instFunLikeDerivationForall_sDG deriv instIsKockLawvere_oneOfIsKockLawvere instInvertibleCastFactorial_sDG	—	instIsKockLawvere_oneOfIsKockLawvere Fin.sum_univ_zero Fin.sum_univ_one inv_factorial_zero Fin.sum_univ_succ taylor_one Fin.sum_snoc_zero Fin.sum_cons_zero mem_D_add_pow mem_D_sum_pow_succ succ_mul_inv_factorial_succ
taylor_k_aux' 📖	mathematical	𝔻 List.Fin.fintype	instFunLikeDerivationForall_sDG deriv instIsKockLawvere_oneOfIsKockLawvere	—	instIsKockLawvere_oneOfIsKockLawvere taylor_k_aux_zero cancel_d_fun 𝔻_le mem_D_sum_pow_succ Fin.sum_univ_succAbove_last Fin.sum_castLe_of_eq_zero inv_factorial_one Fin.sum_univ_succ inv_factorial_zero taylor_k_aux mem_D_sum_pow
taylor_k_aux_zero 📖	mathematical	𝔻 List.Fin.fintype	instFunLikeDerivationForall_sDG deriv instIsKockLawvere_oneOfIsKockLawvere	—	instIsKockLawvere_oneOfIsKockLawvere derivative_unique 𝔻_le Fin.sum_univ_succ
taylor_two 📖	mathematical	—	𝔻 instFunLikeDerivationForall_sDG deriv instIsKockLawvere_oneOfIsKockLawvere	—	instIsKockLawvere_oneOfIsKockLawvere IsKockLawvere.isKockLawvere derivative_unique 𝔻_pow Fin.sum_univ_two 𝔻_le D_add_sq taylor_two_aux mem_𝔻_of_mem_D_add_mem_D cancel_d

---

← Back to Index