Documentation Verification Report

ScalarPotential

📁 Source: PhysLean/Electromagnetism/Kinematics/ScalarPotential.lean

Statistics

MetricCount
DefinitionsscalarPotential, scalarPotential
2
TheoremsscalarPotential_contDiff, scalarPotential_contDiff_space, scalarPotential_contDiff_time, scalarPotential_differentiable, scalarPotential_differentiable_space, scalarPotential_differentiable_time
6
Total8

Electromagnetism.DistElectromagneticPotential

Definitions

NameCategoryTheorems
scalarPotential 📖CompOp
3 mathmath: oneDimPointParticle_scalarPotential, threeDimPointParticle_scalarPotential, infiniteWire_scalarPotential

Electromagnetism.ElectromagneticPotential

Definitions

NameCategoryTheorems
scalarPotential 📖CompOp
15 mathmath: hamiltonian_eq_electricField_scalarPotential, hamiltonian_eq_electricField_magneticField, scalarPotential_contDiff_space, scalarPotential_differentiable_time, electricField_eq, scalarPotential_contDiff, scalarPotential_differentiable_space, time_deriv_comp_vectorPotential_eq_electricField, harmonicWaveX_scalarPotential_eq_zero, scalarPotential_differentiable, time_deriv_vectorPotential_eq_electricField, freeCurrentPotential_eq_sum_scalarPotential_vectorPotential, constantEB_scalarPotential, lagrangian_eq_electric_magnetic, scalarPotential_contDiff_time

Theorems

NameKindAssumesProvesValidatesDepends On
scalarPotential_contDiff 📖mathematicalSpaceTime
Lorentz.Vector.isNormedAddCommGroup
Lorentz.Vector.isNormedSpace
Lorentz.Vector
Time
Space
Time.instNormedAddCommGroup
Space.instNormedAddCommGroup
Time.instNormedSpaceReal
Space.instInnerProductSpaceReal
scalarPotential
SpaceTime.timeSlice_contDiff
SpaceTime.contDiff_vector
scalarPotential_contDiff_space 📖mathematicalSpaceTime
Lorentz.Vector.isNormedAddCommGroup
Lorentz.Vector.isNormedSpace
Lorentz.Vector
Space
Space.instNormedAddCommGroup
Space.instInnerProductSpaceReal
scalarPotential
scalarPotential_contDiff
scalarPotential_contDiff_time 📖mathematicalSpaceTime
Lorentz.Vector.isNormedAddCommGroup
Lorentz.Vector.isNormedSpace
Lorentz.Vector
Time
Time.instNormedAddCommGroup
Time.instNormedSpaceReal
scalarPotential
scalarPotential_contDiff
scalarPotential_differentiable 📖mathematicalSpaceTime
Lorentz.Vector.instAddCommGroup
Lorentz.Vector.instModuleReal
Lorentz.Vector.isNormedAddCommGroup
Lorentz.Vector
Time
Space
Time.instAddCommGroup
Space.instAddCommGroup
Time.instSeminormedAddCommGroup
Time.instNormedAddCommGroup
Space.instAddCommMonoid
Time.instModuleReal
Space.instModuleReal
Space.instSeminormedAddCommGroup
scalarPotential
SpaceTime.timeSlice_differentiable
SpaceTime.differentiable_vector
scalarPotential_differentiable_space 📖mathematicalSpaceTime
Lorentz.Vector.instAddCommGroup
Lorentz.Vector.instModuleReal
Lorentz.Vector.isNormedAddCommGroup
Lorentz.Vector
Space
Space.instAddCommGroup
Space.instModuleReal
Space.instSeminormedAddCommGroup
scalarPotential
scalarPotential_differentiable
scalarPotential_differentiable_time 📖mathematicalSpaceTime
Lorentz.Vector.instAddCommGroup
Lorentz.Vector.instModuleReal
Lorentz.Vector.isNormedAddCommGroup
Lorentz.Vector
Time
Time.instAddCommGroup
Time.instModuleReal
Time.instSeminormedAddCommGroup
scalarPotential
scalarPotential_differentiable

---

← Back to Index