Documentation Verification Report

Deriv

📁 Source: SDG/IsKockLawvere_one/Deriv.lean

Statistics

Metric	Count
Definitions `deriv`, `instFunLikeDerivationForall_sDG`, `«term∂^[_]»`, `«term∂_»`	4
Theorems `chain_rule`, `chain_rulefun`, `derivFun_spec`, `derivFun_taylor_one`, `derivFun_unique`, `deriv_X_pow`, `deriv_const`, `deriv_equiv`, `deriv_inv`, `deriv_mul`, `derivative_id`, `derivative_spec`, `derivative_unique`, `taylor_one`, `taylor_two_aux`	15
Total	19

SDG

Definitions

Name	Category	Theorems
`deriv` 📖	CompOp	17 math math: `taylor_k_aux_zero`, `deriv_inv`, `taylor_one`, `derivative_unique`, `taylor_k_aux'`, `deriv_const`, `taylor_two`, `derivative_id`, `taylor_k_aux`, `chain_rulefun`, `taylor_k`, `deriv_equiv`, `deriv_mul`, `chain_rule`, `taylor_two_aux`, `deriv_X_pow`, `derivative_spec`
`instFunLikeDerivationForall_sDG` 📖	CompOp	17 math math: `taylor_k_aux_zero`, `deriv_inv`, `taylor_one`, `derivative_unique`, `taylor_k_aux'`, `deriv_const`, `taylor_two`, `derivative_id`, `taylor_k_aux`, `chain_rulefun`, `taylor_k`, `deriv_equiv`, `deriv_mul`, `chain_rule`, `taylor_two_aux`, `deriv_X_pow`, `derivative_spec`
`«term∂^[_]»` 📖	CompOp	—
`«term∂_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`chain_rule` 📖	mathematical	—	`instFunLikeDerivationForall_sDG` `deriv`	—	`derivative_unique` `D_mul_mem` `taylor_one`
`chain_rulefun` 📖	mathematical	—	`instFunLikeDerivationForall_sDG` `deriv`	—	`chain_rule`
`derivFun_spec` 📖	mathematical	—	`D` `derivFun`	—	`unique_choice_fun.congr_simp` `IsKockLawvere_one.isKockLawvere_one` `unique_choice_fun_spec`
`derivFun_taylor_one` 📖	mathematical	—	`D` `derivFun`	—	`unique_choice_fun.congr_simp` `IsKockLawvere_one.isKockLawvere_one` `unique_choice_fun_spec`
`derivFun_unique` 📖	mathematical	`D`	`derivFun`	—	`cancel_d` `derivFun_taylor_one`
`deriv_X_pow` 📖	mathematical	—	`instFunLikeDerivationForall_sDG` `deriv`	—	`derivative_unique` `deriv_mul` `derivative_id`
`deriv_const` 📖	mathematical	—	`instFunLikeDerivationForall_sDG` `deriv`	—	`derivative_unique`
`deriv_equiv` 📖	mathematical	—	`instFunLikeDerivationForall_sDG` `deriv`	—	`derivative_id` `chain_rulefun`
`deriv_inv` 📖	mathematical	—	`instFunLikeDerivationForall_sDG` `deriv`	—	—
`deriv_mul` 📖	mathematical	—	`instFunLikeDerivationForall_sDG` `deriv`	—	—
`derivative_id` 📖	mathematical	—	`instFunLikeDerivationForall_sDG` `deriv`	—	`derivative_unique`
`derivative_spec` 📖	mathematical	—	`D` `instFunLikeDerivationForall_sDG` `deriv`	—	`derivFun_spec`
`derivative_unique` 📖	mathematical	`D`	`instFunLikeDerivationForall_sDG` `deriv`	—	`derivFun_unique`
`taylor_one` 📖	mathematical	—	`D` `instFunLikeDerivationForall_sDG` `deriv`	—	`derivFun_taylor_one`
`taylor_two_aux` 📖	mathematical	—	`D` `instFunLikeDerivationForall_sDG` `deriv`	—	`taylor_one` `D_add_sq_dvd_two`

---

← Back to Index