Documentation Verification Report

Constant

📁 Source: PhysLean/Electromagnetism/Vacuum/Constant.lean

Statistics

Metric	Count
Definitions `constantEB`	1
Theorems `constantEB_electricField`, `constantEB_isExtrema`, `constantEB_magneticFieldMatrix`, `constantEB_scalarPotential`, `constantEB_smooth`, `constantEB_vectorPotential`, `constantEB_vectorPotential_space_deriv`, `constantEB_vectorPotential_time_deriv`	8
Total	9

Electromagnetism.ElectromagneticPotential

Definitions

Name	Category	Theorems
`constantEB` 📖	CompOp	8 math math: `constantEB_electricField`, `constantEB_vectorPotential_time_deriv`, `constantEB_vectorPotential_space_deriv`, `constantEB_scalarPotential`, `constantEB_isExtrema`, `constantEB_vectorPotential`, `constantEB_magneticFieldMatrix`, `constantEB_smooth`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`constantEB_electricField` 📖	mathematical	—	`electricField` `constantEB`	—	`electricField_eq` `constantEB_scalarPotential` `constantEB_vectorPotential_time_deriv` `Space.grad_neg` `Space.basis_repr_inner_eq` `Space.grad_inner_right`
`constantEB_isExtrema` 📖	mathematical	—	`IsExtrema` `constantEB` `Electromagnetism.FreeSpace.c` `Electromagnetism.LorentzCurrentDensity` `SpaceTime` `Lorentz.Vector` `Lorentz.Vector.instAddCommGroup`	—	`isExtrema_iff_gauss_ampere_magneticFieldMatrix` `constantEB_smooth` `constantEB_electricField` `Space.div_const` `Electromagnetism.LorentzCurrentDensity.chargeDensity_zero` `Time.deriv_const` `constantEB_magneticFieldMatrix` `Space.deriv_const` `Electromagnetism.LorentzCurrentDensity.currentDensity_zero`
`constantEB_magneticFieldMatrix` 📖	mathematical	—	`magneticFieldMatrix` `constantEB`	—	`magneticFieldMatrix_eq_vectorPotential` `constantEB_smooth` `constantEB_vectorPotential_space_deriv`
`constantEB_scalarPotential` 📖	mathematical	—	`scalarPotential` `constantEB` `instInnerOfInnerProductSpace'` `instInnerProductSpace'` `Space` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal` `Space.basis`	—	`SpaceTime.space_toTimeAndSpace_symm`
`constantEB_smooth` 📖	mathematical	—	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector` `constantEB`	—	`Lorentz.Vector.contDiff_apply` `Lorentz.Vector.coord_contDiff`
`constantEB_vectorPotential` 📖	mathematical	—	`vectorPotential` `constantEB` `Space.val`	—	`SpaceTime.space_toCoord_symm` `SpaceTime.toTimeAndSpace_symm_apply_inr`
`constantEB_vectorPotential_space_deriv` 📖	mathematical	—	`Space.deriv` `vectorPotential` `constantEB`	—	`constantEB_vectorPotential` `Space.deriv_eq` `Space.eval_differentiable` `Space.deriv_component_diff` `Space.deriv_component_same`
`constantEB_vectorPotential_time_deriv` 📖	mathematical	—	`Time.deriv` `vectorPotential` `constantEB`	—	`constantEB_vectorPotential` `Time.deriv_const`

---

← Back to Index