Documentation Verification Report

Curl

📁 Source: PhysLean/SpaceAndTime/Space/Derivatives/Curl.lean

Statistics

Metric	Count
Definitions `curl`, `curlNotation`, `distCurl`	3
Theorems `curl_add`, `curl_const`, `curl_linear_map`, `curl_of_curl`, `curl_smul`, `curl_zero`, `deriv_coord_2nd_add`, `deriv_coord_2nd_sub`, `distCurl_apply`, `distCurl_apply_one`, `distCurl_apply_two`, `distCurl_apply_zero`, `distCurl_distGrad_eq_zero`, `div_of_curl_eq_zero`	14
Total	17

Space

Definitions

Name	Category	Theorems
`curl` 📖	CompOp	12 math math: `time_deriv_curl_commute`, `curl_differentiable_time`, `curl_zero`, `Electromagnetism.ElectromagneticPotential.magneticField_eq`, `curl_smul`, `div_of_curl_eq_zero`, `curl_const`, `curl_linear_map`, `Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_electric_magnetic_three`, `curl_add`, `Electromagnetism.ElectromagneticPotential.magneticField_curl_eq_magneticFieldMatrix`, `curl_of_curl`
`curlNotation` 📖	CompOp	—
`distCurl` 📖	CompOp	7 math math: `constantTime_spaceCurlD`, `distCurl_distConst`, `distCurl_apply_two`, `distCurl_apply`, `distCurl_apply_one`, `distCurl_apply_zero`, `distCurl_distGrad_eq_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`curl_add` 📖	mathematical	`Space` `instAddCommGroup` `instModuleReal` `instSeminormedAddCommGroup`	`curl`	—	`deriv_coord_add`
`curl_const` 📖	mathematical	—	`curl` `Space`	—	—
`curl_linear_map` 📖	mathematical	`Space` `instAddCommGroup` `instModuleReal` `instSeminormedAddCommGroup`	`curl`	—	`curl_add` `curl_smul`
`curl_of_curl` 📖	mathematical	`Space` `instNormedAddCommGroup` `instInnerProductSpaceReal`	`curl` `grad` `div` `laplacianVec`	—	`deriv_coord_2nd_sub` `deriv_coord_2nd_add` `deriv_commute`
`curl_smul` 📖	mathematical	`Space` `instAddCommGroup` `instModuleReal` `instSeminormedAddCommGroup`	`curl`	—	`deriv_coord_smul`
`curl_zero` 📖	mathematical	—	`curl` `Space`	—	—
`deriv_coord_2nd_add` 📖	mathematical	`Space` `instNormedAddCommGroup` `instInnerProductSpaceReal`	`deriv`	—	—
`deriv_coord_2nd_sub` 📖	mathematical	`Space` `instNormedAddCommGroup` `instInnerProductSpaceReal`	`deriv`	—	—
`distCurl_apply` 📖	mathematical	—	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distCurl` `basis`	—	`distCurl_apply_zero` `distCurl_apply_one` `distCurl_apply_two`
`distCurl_apply_one` 📖	mathematical	—	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distCurl` `basis`	—	`Distribution.fderivD_apply`
`distCurl_apply_two` 📖	mathematical	—	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distCurl` `basis`	—	`Distribution.fderivD_apply`
`distCurl_apply_zero` 📖	mathematical	—	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distCurl` `basis`	—	`Distribution.fderivD_apply`
`distCurl_distGrad_eq_zero` 📖	mathematical	—	`Distribution` `Space` `instNormedAddCommGroup` `instInnerProductSpaceReal` `distCurl` `distGrad`	—	`distCurl_apply_zero` `distGrad_eq_sum_basis` `schwartMap_fderiv_comm` `distCurl_apply_one` `distCurl_apply_two`
`div_of_curl_eq_zero` 📖	mathematical	`Space` `instNormedAddCommGroup` `instInnerProductSpaceReal`	`div` `curl`	—	`deriv_coord_2nd_sub` `deriv_commute`

---

← Back to Index