Electromagnetism

In this file we define the electric field, the magnetic field, and the field strength tensor.

@[reducible, inline]

abbrev Electromagnetism.ElectricField (d : ℕ := 3) : Type

The electric field is a map from d+1 dimensional spacetime to the vector space ℝ^d.

Equations

• Electromagnetism.ElectricField d = (Time → Space d → EuclideanSpace ℝ (Fin d))

@[reducible, inline]

abbrev Electromagnetism.MagneticField (d : ℕ := 3) : Type

The magnetic field is a map from d+1 dimensional spacetime to the vector space ℝ^d.

Equations

• Electromagnetism.MagneticField d = (Time → Space d → EuclideanSpace ℝ (Fin d))

@[reducible, inline]

abbrev Electromagnetism.VectorPotential (d : ℕ := 3) : Type

The vector potential of an electromagnetic field

Equations

• Electromagnetism.VectorPotential d = (SpaceTime d → (realLorentzTensor d).Tensor ![realLorentzTensor.Color.up])