Documentation Verification Report

PartialDeriv

📁 Source: SDG/IsKockLawvere_one/PartialDeriv.lean

Statistics

Metric	Count
Definitions `instFunLikeDerivationForallForallFin_sDG`, `partial_deriv`, `partial_derivFun`, `«term∂[_]_»`	4
Theorems `partial_derivFun_spec`, `partial_derivFun_unique`, `partial_deriv_comm`, `partial_deriv_const`, `partial_deriv_mul`, `partial_deriv_proj_ne`, `partial_deriv_proj_self`, `partial_deriv_propr`, `partial_derivative_unique`, `partial_taylor_one`	10
Total	14

SDG

Definitions

Name	Category	Theorems
`instFunLikeDerivationForallForallFin_sDG` 📖	CompOp	7 math math: `partial_taylor_one`, `partial_deriv_proj_self`, `partial_deriv_const`, `partial_deriv_proj_ne`, `partial_derivative_unique`, `partial_deriv_comm`, `partial_deriv_mul`
`partial_deriv` 📖	CompOp	7 math math: `partial_taylor_one`, `partial_deriv_proj_self`, `partial_deriv_const`, `partial_deriv_proj_ne`, `partial_derivative_unique`, `partial_deriv_comm`, `partial_deriv_mul`
`partial_derivFun` 📖	CompOp	2 math math: `partial_derivFun_unique`, `partial_derivFun_spec`
`«term∂[_]_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`partial_derivFun_spec` 📖	mathematical	—	`D` `partial_derivFun`	—	`unique_choice_fun_spec` `partial_deriv_propr`
`partial_derivFun_unique` 📖	mathematical	`D`	`partial_derivFun`	—	`unique_choice_fun_unique` `partial_deriv_propr`
`partial_deriv_comm` 📖	mathematical	—	`instFunLikeDerivationForallForallFin_sDG` `partial_deriv`	—	`partial_deriv.congr_simp` `cancel_d` `partial_taylor_one` `Function.update_update_comm`
`partial_deriv_const` 📖	mathematical	—	`instFunLikeDerivationForallForallFin_sDG` `partial_deriv`	—	`partial_derivative_unique`
`partial_deriv_mul` 📖	mathematical	—	`instFunLikeDerivationForallForallFin_sDG` `partial_deriv`	—	—
`partial_deriv_proj_ne` 📖	mathematical	—	`instFunLikeDerivationForallForallFin_sDG` `partial_deriv`	—	`partial_derivative_unique`
`partial_deriv_proj_self` 📖	mathematical	—	`instFunLikeDerivationForallForallFin_sDG` `partial_deriv`	—	`partial_derivative_unique`
`partial_deriv_propr` 📖	—	—	—	—	`IsKockLawvere_one.isKockLawvere_one` `coe_zero` `Function.update_eq_self`
`partial_derivative_unique` 📖	mathematical	`D`	`instFunLikeDerivationForallForallFin_sDG` `partial_deriv`	—	`partial_derivFun_unique`
`partial_taylor_one` 📖	mathematical	—	`D` `instFunLikeDerivationForallForallFin_sDG` `partial_deriv`	—	`partial_derivFun_spec`

---

← Back to Index