@[reducible, inline]
The type of static electric fields (i.e. time-independent electric fields), defined
as distributions from Space d
to EuclideanSpace ℝ (Fin d)
.
Equations
- Electromagnetism.StaticElectricField d = ((Space d)→d[ℝ] EuclideanSpace ℝ (Fin d))
Instances For
noncomputable def
Electromagnetism.StaticElectricField.ofPotential
{d : ℕ}
(φ : StaticElectricPotential d)
:
The static electric field associated with a static electric potential.
Instances For
def
Electromagnetism.StaticElectricField.GaussLaw
{d : ℕ}
(E : StaticElectricField d)
(ε : ℝ)
(ρ : ChargeDistribution d)
:
Gauss's law for static electric fields.
Instances For
theorem
Electromagnetism.StaticElectricField.gaussLaw_iff
{d : ℕ}
(E : StaticElectricField d)
(ε : ℝ)
(ρ : ChargeDistribution d)
:
Faraday's law in 3d for static electric fields.
Equations
- E.FaradaysLaw = (Space.curlD E = 0)
Instances For
theorem
Electromagnetism.StaticElectricField.ofPotential_faradaysLaw
(φ : StaticElectricPotential)
:
If the electric field is of the form -∇φ
then Faraday's law holds.