MagneticField

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

Statistics

Metric	Count
Definitions `magneticFieldMatrix`, `magneticField`, `magneticFieldMatrix`, `MagneticField`	4
Theorems `magneticFieldMatrix_basis_repr_eq_fieldStrength`, `magneticFieldMatrix_basis_repr_eq_vector_potential`, `magneticFieldMatrix_distSpaceDeriv_basis_repr_eq_vector_potential`, `magneticFieldMatrix_eq_vectorPotential`, `magneticFieldMatrix_one_dim_eq_zero`, `curl_magneticFieldMatrix_eq_electricField_fieldStrengthMatrix`, `fieldStrengthMatrix_eq_electric_magnetic`, `fieldStrengthMatrix_eq_electric_magnetic_of_spaceTime`, `fieldStrengthMatrix_inr_inr_eq_magneticFieldMatrix`, `magneticFieldMatrix_antisymm`, `magneticFieldMatrix_contDiff`, `magneticFieldMatrix_diag_eq_zero`, `magneticFieldMatrix_differentiable`, `magneticFieldMatrix_differentiable_space`, `magneticFieldMatrix_differentiable_time`, `magneticFieldMatrix_eq`, `magneticFieldMatrix_eq_vectorPotential`, `magneticFieldMatrix_space_contDiff`, `magneticFieldMatrix_space_deriv_eq`, `magneticFieldMatrix_time_contDiff`, `magneticField_curl_eq_magneticFieldMatrix`, `magneticField_div_eq_zero`, `magneticField_eq`, `magneticField_eq_magneticFieldMatrix`, `magneticField_fst_eq_fieldStrengthMatrix`, `magneticField_snd_eq_fieldStrengthMatrix`, `magneticField_thd_eq_fieldStrengthMatrix`, `time_deriv_magneticFieldMatrix`, `time_deriv_time_deriv_magneticFieldMatrix`	29
Total	33

Electromagnetism

Definitions

Name	Category	Theorems
`MagneticField` 📖	CompOp	—

Electromagnetism.DistElectromagneticPotential

Definitions

Name	Category	Theorems
`magneticFieldMatrix` 📖	CompOp	10 math math: `gradLagrangian_sum_inr_i`, `isExtrema_iff_space_time`, `magneticFieldMatrix_eq_vectorPotential`, `magneticFieldMatrix_basis_repr_eq_fieldStrength`, `gradKineticTerm_sum_inr_eq`, `magneticFieldMatrix_basis_repr_eq_vector_potential`, `threeDimPointParticle_magneticFieldMatrix`, `magneticFieldMatrix_distSpaceDeriv_basis_repr_eq_vector_potential`, `magneticFieldMatrix_one_dim_eq_zero`, `oneDimPointParticle_magneticFieldMatrix`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`magneticFieldMatrix_basis_repr_eq_fieldStrength` 📖	mathematical	—	`Distribution` `Time` `Space` `Time.instNormedAddCommGroup` `Space.instNormedAddCommGroup` `Time.instNormedSpaceReal` `Space.instInnerProductSpaceReal` `Electromagnetism.DistElectromagneticPotential` `SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instAddCommGroup` `magneticFieldMatrix` `Lorentz.Vector.basis` `Lorentz.Vector.innerProductSpace` `SpaceTime.distTimeSlice` `fieldStrength`	—	`magneticFieldMatrix_eq_vectorPotential` `SpaceTime.distTimeSlice_apply` `fieldStrength_basis_repr_eq_single` `minkowskiMatrix.inr_i_inr_i` `Space.distSpaceDeriv_apply_CLM` `SpaceTime.distTimeSlice_distDeriv_inr`
`magneticFieldMatrix_basis_repr_eq_vector_potential` 📖	mathematical	—	`Distribution` `Time` `Space` `Time.instNormedAddCommGroup` `Space.instNormedAddCommGroup` `Time.instNormedSpaceReal` `Space.instInnerProductSpaceReal` `Electromagnetism.DistElectromagneticPotential` `SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instAddCommGroup` `magneticFieldMatrix` `Space.distSpaceDeriv` `vectorPotential`	—	`magneticFieldMatrix_eq_vectorPotential`
`magneticFieldMatrix_distSpaceDeriv_basis_repr_eq_vector_potential` 📖	mathematical	—	`Distribution` `Time` `Space` `Time.instNormedAddCommGroup` `Space.instNormedAddCommGroup` `Time.instNormedSpaceReal` `Space.instInnerProductSpaceReal` `Space.distSpaceDeriv` `Electromagnetism.DistElectromagneticPotential` `SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instAddCommGroup` `magneticFieldMatrix` `vectorPotential`	—	`Space.distSpaceDeriv_apply'` `magneticFieldMatrix_basis_repr_eq_vector_potential`
`magneticFieldMatrix_eq_vectorPotential` 📖	mathematical	—	`Distribution` `Time` `Space` `Time.instNormedAddCommGroup` `Space.instNormedAddCommGroup` `Time.instNormedSpaceReal` `Space.instInnerProductSpaceReal` `Electromagnetism.DistElectromagneticPotential` `SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instAddCommGroup` `magneticFieldMatrix` `Space.distSpaceDeriv` `vectorPotential`	—	`SpaceTime.distTimeSlice_apply` `fieldStrength_eq_basis` `minkowskiMatrix.inl_0_inl_0` `minkowskiMatrix.inr_i_inr_i` `Lorentz.Vector.spatialCLM_basis_sum_inl` `Lorentz.Vector.spatialCLM_basis_sum_inr` `SpaceTime.distTimeSlice_distDeriv_inr` `Space.distSpaceDeriv_apply_CLM`
`magneticFieldMatrix_one_dim_eq_zero` 📖	mathematical	—	`Electromagnetism.DistElectromagneticPotential` `Distribution` `Time` `Space` `Time.instNormedAddCommGroup` `Space.instNormedAddCommGroup` `Time.instNormedSpaceReal` `Space.instInnerProductSpaceReal` `SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instAddCommGroup` `magneticFieldMatrix`	—	`magneticFieldMatrix_eq_vectorPotential`

Electromagnetism.ElectromagneticPotential

Definitions

Name	Category	Theorems
`magneticField` 📖	CompOp	12 math math: `kineticTerm_eq_electric_magnetic'`, `magneticField_eq`, `fieldStrengthMatrix_eq_electric_magnetic`, `magneticField_snd_eq_fieldStrengthMatrix`, `kineticTerm_eq_electric_magnetic`, `magneticField_thd_eq_fieldStrengthMatrix`, `magneticField_fst_eq_fieldStrengthMatrix`, `gradKineticTerm_eq_electric_magnetic_three`, `magneticField_eq_magneticFieldMatrix`, `magneticField_curl_eq_magneticFieldMatrix`, `magneticField_div_eq_zero`, `fieldStrengthMatrix_eq_electric_magnetic_of_spaceTime`
`magneticFieldMatrix` 📖	CompOp	46 math math: `IsPlaneWave.magneticFieldMatrix_eq_propogator_cross_electricField`, `hamiltonian_eq_electricField_magneticField`, `magneticFieldMatrix_space_contDiff`, `IsPlaneWave.magneticFunction_eq_magneticFieldMatrix`, `time_deriv_magneticFieldMatrix`, `harmonicWaveX_magneticFieldMatrix_space_deriv_succ`, `IsPlaneWave.magneticFieldMatrix_time_deriv`, `magneticFieldMatrix_space_deriv_eq`, `magneticFieldMatrix_differentiable_space`, `magneticFieldMatrix_differentiable_time`, `curl_magneticFieldMatrix_eq_electricField_fieldStrengthMatrix`, `gradKineticTerm_eq_electric_magnetic`, `harmonicWaveX_magneticFieldMatrix_zero_succ`, `time_deriv_time_deriv_magneticFieldMatrix`, `gradLagrangian_eq_electricField_magneticField`, `IsPlaneWave.space_deriv_electricField_eq_magneticFieldMatrix`, `IsPlaneWave.time_deriv_electricField_eq_magneticFieldMatrix`, `IsPlaneWave.magneticFieldMatrix_space_deriv`, `magneticFieldMatrix_contDiff`, `IsPlaneWave.magneticFieldMatrix_eq_magneticFunction`, `time_deriv_time_deriv_magneticFieldMatrix_of_isExtrema`, `harmonicWaveX_magneticFieldMatrix_succ_zero`, `kineticTerm_eq_electricMatrix_magneticFieldMatrix_time_space`, `magneticFieldMatrix_diag_eq_zero`, `magneticFieldMatrix_apply_x_boost_succ_succ`, `magneticFieldMatrix_differentiable`, `IsPlaneWave.space_deriv_magneticFieldMatrix_eq_electricField_mul_propogator`, `magneticFieldMatrix_eq_vectorPotential`, `magneticField_eq_magneticFieldMatrix`, `magneticField_curl_eq_magneticFieldMatrix`, `magneticFieldMatrix_antisymm`, `harmonicWaveX_magneticFieldMatrix_succ_succ`, `constantEB_magneticFieldMatrix`, `IsPlaneWave.electricField_eq_propogator_cross_magneticFieldMatrix`, `magneticFieldMatrix_eq`, `magneticFieldMatrix_apply_x_boost_zero_succ`, `IsPlaneWave.magneticFieldMatrix_space_deriv_eq_time_deriv`, `IsPlaneWave.time_deriv_magneticFieldMatrix_eq_electricField_mul_propogator`, `lagrangian_eq_electric_magnetic`, `isExtrema_iff_gauss_ampere_magneticFieldMatrix`, `harmonicWaveX_magneticFieldMatrix_zero_succ_space_deriv_zero`, `kineticTerm_eq_electricMatrix_magneticFieldMatrix`, `electricField_apply_x_boost_succ`, `fieldStrengthMatrix_inr_inr_eq_magneticFieldMatrix`, `time_deriv_electricField_of_isExtrema`, `magneticFieldMatrix_time_contDiff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`curl_magneticFieldMatrix_eq_electricField_fieldStrengthMatrix` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Space.deriv` `magneticFieldMatrix` `SpeedOfLight.val` `Time.deriv` `electricField` `SpaceTime.deriv` `fieldStrengthMatrix` `Time` `Space` `Time.instSeminormedAddCommGroup` `Space.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `Space.instAddCommMonoid` `Lorentz.Vector.instAddCommMonoid` `Time.instModuleReal` `Space.instModuleReal` `Lorentz.Vector.instModuleReal` `SpaceTime.toTimeAndSpace`	—	`time_deriv_electricField_eq_fieldStrengthMatrix` `SpaceTime.deriv_sum_inr` `fieldStrengthMatrix_differentiable`
`fieldStrengthMatrix_eq_electric_magnetic` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector`	`fieldStrengthMatrix` `Time` `Space` `Time.instSeminormedAddCommGroup` `Space.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `Space.instAddCommMonoid` `Lorentz.Vector.instAddCommMonoid` `Time.instModuleReal` `Space.instModuleReal` `SpaceTime.toTimeAndSpace` `electricField` `SpeedOfLight.val` `magneticField`	—	`fieldStrengthMatrix_diag_eq_zero` `electricField_eq_fieldStrengthMatrix` `fieldStrengthMatrix_antisymm` `magneticField_thd_eq_fieldStrengthMatrix` `magneticField_snd_eq_fieldStrengthMatrix` `magneticField_fst_eq_fieldStrengthMatrix`
`fieldStrengthMatrix_eq_electric_magnetic_of_spaceTime` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector`	`fieldStrengthMatrix` `electricField` `Time` `Space` `Lorentz.Vector.instAddCommMonoid` `Time.instSeminormedAddCommGroup` `Space.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `Space.instAddCommMonoid` `Time.instModuleReal` `Space.instModuleReal` `SpaceTime.toTimeAndSpace` `SpeedOfLight.val` `magneticField`	—	`fieldStrengthMatrix_eq_electric_magnetic`
`fieldStrengthMatrix_inr_inr_eq_magneticFieldMatrix` 📖	mathematical	—	`fieldStrengthMatrix` `magneticFieldMatrix` `SpaceTime` `Time` `Lorentz.Vector.instAddCommMonoid` `Time.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `Lorentz.Vector.instModuleReal` `Time.instModuleReal` `SpaceTime.time` `Lorentz.Vector.isNormedAddCommGroup` `Space` `Space.instSeminormedAddCommGroup` `Space.instAddCommMonoid` `Space.instModuleReal` `SpaceTime.space`	—	`magneticFieldMatrix_eq` `SpaceTime.toTimeAndSpace_symm_apply_time_space`
`magneticFieldMatrix_antisymm` 📖	mathematical	—	`magneticFieldMatrix`	—	`magneticFieldMatrix_eq` `fieldStrengthMatrix_antisymm`
`magneticFieldMatrix_contDiff` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Time` `Space` `Time.instNormedAddCommGroup` `Space.instNormedAddCommGroup` `Time.instNormedSpaceReal` `Space.instInnerProductSpaceReal` `magneticFieldMatrix`	—	`fieldStrengthMatrix_contDiff`
`magneticFieldMatrix_diag_eq_zero` 📖	mathematical	—	`magneticFieldMatrix`	—	`magneticFieldMatrix_eq` `fieldStrengthMatrix_diag_eq_zero`
`magneticFieldMatrix_differentiable` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Time` `Space` `Time.instAddCommGroup` `Space.instAddCommGroup` `Time.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `Space.instAddCommMonoid` `Time.instModuleReal` `Space.instModuleReal` `Space.instSeminormedAddCommGroup` `magneticFieldMatrix`	—	`fieldStrengthMatrix_differentiable`
`magneticFieldMatrix_differentiable_space` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Space` `Space.instAddCommGroup` `Space.instModuleReal` `Space.instSeminormedAddCommGroup` `magneticFieldMatrix`	—	`magneticFieldMatrix_differentiable`
`magneticFieldMatrix_differentiable_time` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Time` `Time.instAddCommGroup` `Time.instModuleReal` `Time.instSeminormedAddCommGroup` `magneticFieldMatrix`	—	`magneticFieldMatrix_differentiable`
`magneticFieldMatrix_eq` 📖	mathematical	—	`magneticFieldMatrix` `fieldStrengthMatrix` `Time` `Space` `Time.instSeminormedAddCommGroup` `Space.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `Space.instAddCommMonoid` `SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.instAddCommMonoid` `Time.instModuleReal` `Space.instModuleReal` `Lorentz.Vector.instModuleReal` `SpaceTime.toTimeAndSpace`	—	—
`magneticFieldMatrix_eq_vectorPotential` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector`	`magneticFieldMatrix` `Space.deriv` `vectorPotential`	—	`magneticFieldMatrix_eq` `toFieldStrength_basis_repr_apply_eq_single` `minkowskiMatrix.inr_i_inr_i` `SpaceTime.deriv_sum_inr` `Space.deriv_lorentz_vector`
`magneticFieldMatrix_space_contDiff` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Space` `Space.instNormedAddCommGroup` `Space.instInnerProductSpaceReal` `magneticFieldMatrix`	—	`magneticFieldMatrix_contDiff`
`magneticFieldMatrix_space_deriv_eq` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Space.deriv` `magneticFieldMatrix`	—	`magneticFieldMatrix_eq_vectorPotential` `Space.deriv_eq_fderiv_basis` `Space.deriv_differentiable` `vectorPotential_apply_contDiff_space` `Space.deriv_commute`
`magneticFieldMatrix_time_contDiff` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Time` `Time.instNormedAddCommGroup` `Time.instNormedSpaceReal` `magneticFieldMatrix`	—	`magneticFieldMatrix_contDiff`
`magneticField_curl_eq_magneticFieldMatrix` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Space.curl` `magneticField` `Space.deriv` `magneticFieldMatrix`	—	`magneticField_eq_magneticFieldMatrix` `Space.deriv_eq_fderiv_basis` `magneticFieldMatrix_diag_eq_zero` `magneticFieldMatrix_antisymm`
`magneticField_div_eq_zero` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Space.div` `magneticField` `Space`	—	`magneticField_eq` `Space.div_of_curl_eq_zero` `vectorPotential_contDiff_space`
`magneticField_eq` 📖	mathematical	—	`magneticField` `Space.curl` `vectorPotential`	—	—
`magneticField_eq_magneticFieldMatrix` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector`	`magneticField` `magneticFieldMatrix`	—	`magneticFieldMatrix_eq` `magneticField_fst_eq_fieldStrengthMatrix` `magneticField_snd_eq_fieldStrengthMatrix` `magneticField_thd_eq_fieldStrengthMatrix`
`magneticField_fst_eq_fieldStrengthMatrix` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector`	`magneticField` `fieldStrengthMatrix` `Time` `Space` `Time.instSeminormedAddCommGroup` `Space.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `Space.instAddCommMonoid` `Lorentz.Vector.instAddCommMonoid` `Time.instModuleReal` `Space.instModuleReal` `SpaceTime.toTimeAndSpace`	—	`toFieldStrength_basis_repr_apply_eq_single` `minkowskiMatrix.inr_i_inr_i` `magneticField.eq_1` `SpaceTime.deriv_sum_inr` `Space.deriv_eq` `Lorentz.Vector.fderiv_apply`
`magneticField_snd_eq_fieldStrengthMatrix` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector`	`magneticField` `fieldStrengthMatrix` `Time` `Space` `Time.instSeminormedAddCommGroup` `Space.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `Space.instAddCommMonoid` `Lorentz.Vector.instAddCommMonoid` `Time.instModuleReal` `Space.instModuleReal` `SpaceTime.toTimeAndSpace`	—	`toFieldStrength_basis_repr_apply_eq_single` `minkowskiMatrix.inr_i_inr_i` `magneticField.eq_1` `SpaceTime.deriv_sum_inr` `Space.deriv_eq` `Lorentz.Vector.fderiv_apply`
`magneticField_thd_eq_fieldStrengthMatrix` 📖	mathematical	`SpaceTime` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector`	`magneticField` `fieldStrengthMatrix` `Time` `Space` `Time.instSeminormedAddCommGroup` `Space.instSeminormedAddCommGroup` `Time.instNormedAddCommGroup` `Space.instAddCommMonoid` `Lorentz.Vector.instAddCommMonoid` `Time.instModuleReal` `Space.instModuleReal` `SpaceTime.toTimeAndSpace`	—	`toFieldStrength_basis_repr_apply_eq_single` `minkowskiMatrix.inr_i_inr_i` `magneticField.eq_1` `SpaceTime.deriv_sum_inr` `Space.deriv_eq` `Lorentz.Vector.fderiv_apply`
`time_deriv_magneticFieldMatrix` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Time.deriv` `magneticFieldMatrix` `Space.deriv` `electricField`	—	`magneticFieldMatrix_eq_vectorPotential` `Time.deriv.eq_1` `Space.space_deriv_differentiable_time` `vectorPotential_comp_contDiff` `Space.time_deriv_comm_space_deriv` `time_deriv_comp_vectorPotential_eq_electricField` `Space.deriv_eq_fderiv_basis` `electricField_apply_differentiable_space` `Space.deriv_differentiable` `scalarPotential_contDiff_space` `Space.deriv_commute`
`time_deriv_time_deriv_magneticFieldMatrix` 📖	mathematical	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector`	`Time.deriv` `magneticFieldMatrix` `Space.deriv` `electricField`	—	`time_deriv_magneticFieldMatrix` `Time.deriv.eq_1` `Space.space_deriv_differentiable_time` `electricField_apply_contDiff` `Space.time_deriv_comm_space_deriv` `Time.deriv_euclid` `electricField_differentiable_time`

---

← Back to Index