Physlib.Electromagnetism.Dynamics.Basic

For any free space $\mathcal{F}$ with electric permittivity $\epsilon_0$, it holds that $0 \le \epsilon_0$.

For any free space $\mathcal{F}$ with magnetic permeability $\mu_0$, it holds that $0 \le \mu_0$.

For any free space $\mathcal{F}$ with electric permittivity $\epsilon_0$, it holds that $\epsilon_0 \neq 0$.

For any free space $\mathcal{F}$ with magnetic permeability $\mu_0$, it holds that $\mu_0 \neq 0$.

Given a free space $\mathcal{F}$ with electric permittivity $\epsilon_0$ and magnetic permeability $\mu_0$, the speed of light $c$ is defined by the relation $$c = \frac{1}{\sqrt{\epsilon_0 \mu_0}}$$ This definition includes a proof that $c$ is a positive value, as required by the `SpeedOfLight` type.

For any free space $\mathcal{F}$ with electric permittivity $\epsilon_0$ and magnetic permeability $\mu_0$, the speed of light $c$ is given by the relation $$c = \frac{1}{\sqrt{\epsilon_0 \mu_0}}$$

For any free space $\mathcal{F}$ with electric permittivity $\epsilon_0$ and magnetic permeability $\mu_0$, the square of the speed of light $c$ is given by the relation $$c^2 = \frac{1}{\epsilon_0 \mu_0}$$

For any free space $\mathcal{F}$, the speed of light $c$ in that space satisfies the property that its absolute value is equal to itself, i.e., $|c| = c$.