1. Physlib
  2. Electromagnetism
  3. Kinematics
  4. FieldStrength
Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.Electromagnetism.Kinematics.EMPotential public import Physlib.Relativity.Tensors.RealTensor.Metrics.Basic public import Mathlib.Algebra.Order.Archimedean.Real.Hom

The Field Strength Tensor

i. Overview

In this module we define the field strength tensor in terms of the electromagnetic potential.

We define a tensor version and a matrix version and prover various properties of these.

ii. Key results

    toFieldStrength : The field strength tensor from an electromagnetic potential.

    fieldStrengthMatrix : The field strength matrix from an electromagnetic potential (matrix representation of the field strength tensor in the standard basis).

iii. Table of contents

    A. The field strength tensor

      A.1. Tensor equalities

      A.2. Vector equalities

      A.3. The group action acting on the field strength tensor

      A.4. Differentiability and smoothness of the field strength tensor

      A.5. Elements of the field strength tensor in terms of basis

        A.5.1. Index evaluation

      A.6. The field strength matrix

        A.6.1. Differentiability of the field strength matrix

      A.7. The antisymmetry of the field strength tensor

      A.8. Equivariance of the field strength matrix

      A.9. Linearity of the field strength tensor

iv. References

@[expose] public sectionattribute [-simp] Fintype.sum_sum_typeattribute [-simp] Nat.succ_eq_add_oneTODO "Currently the API for the field strength tensor has the definition of `fieldStrengthMatrix`. This is now unneeded, and should be replaced with `toField {A.toFieldStrength x| [μ] [ν]}ᵀ` and suitble API around that. To undertake this TODO, it is likely easier to start building the API around `toField {A.toFieldStrength x| [μ] [ν]}ᵀ` and then remove `fieldStrengthMatrix` once the API is in place."

A. The field strength tensor

We define the field strength tensor F^{μν} in terms of the derivative of the electromagnetic potential A^μ. We then prove that this tensor transforms correctly under Lorentz transformations.

A.1. Tensor equalities

These equalities for the field strength tensor are in terms of tensor expressions and index notation. In practice, we don't expect them to be used explicitly. They are useful for proving some of the API within this module.

All goals completed! 🐙All goals completed! 🐙lemma toFieldStrength_eq_add {d} (A : ElectromagneticPotential d) (x : SpaceTime d) : toFieldStrength A x = Tensorial.toTensor.symm (permT id (IsReindexing.auto) {(η d | μ μ' ⊗ A.deriv x | μ' ν)}ᵀ) - Tensorial.toTensor.symm (permT ![1, 0] (IsReindexing.auto) {(η d | μ μ' ⊗ A.deriv x | μ' ν)}ᵀ) := d:ℕA:ElectromagneticPotential dx:SpaceTime d⊢ A.toFieldStrength x = toTensor.symm ((permT id ⋯) ((contrT 2 1 2 ⋯) ((prodT (contrMetric d)) (toTensor (A.deriv x))))) - toTensor.symm ((permT ![1, 0] ⋯) ((contrT 2 1 2 ⋯) ((prodT (contrMetric d)) (toTensor (A.deriv x))))) d:ℕA:ElectromagneticPotential dx:SpaceTime d⊢ toTensor.symm ((permT id toFieldStrength._proof_3) ((contrT 2 1 2 ⋯) ((prodT (contrMetric d)) (toTensor (A.deriv x))))) + -toTensor.symm ((permT (![1, 0] ∘ id) ⋯) ((contrT 2 1 2 ⋯) ((prodT (contrMetric d)) (toTensor (A.deriv x))))) = toTensor.symm ((permT id ⋯) ((contrT 2 1 2 ⋯) ((prodT (contrMetric d)) (toTensor (A.deriv x))))) + -toTensor.symm ((permT ![1, 0] ⋯) ((contrT 2 1 2 ⋯) ((prodT (contrMetric d)) (toTensor (A.deriv x))))) All goals completed! 🐙lemma toFieldStrength_eq_sub_tensorDeriv {d} {A : ElectromagneticPotential d} (hA : Differentiable ℝ A) (x : SpaceTime d) : toFieldStrength A x = Tensorial.toTensor.symm (permT id IsReindexing.auto {η d | μ μ' ⊗ tensorDeriv A x | μ' ν}ᵀ) - Tensorial.toTensor.symm (permT ![1, 0] IsReindexing.auto {η d | μ μ' ⊗ tensorDeriv A x | μ' ν}ᵀ) := d:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime d⊢ A.toFieldStrength x = toTensor.symm ((permT id ⋯) ((contrT 2 1 2 ⋯) ((prodT (contrMetric d)) (toTensor (tensorDeriv A.val x))))) - toTensor.symm ((permT ![1, 0] ⋯) ((contrT 2 1 2 ⋯) ((prodT (contrMetric d)) (toTensor (tensorDeriv A.val x))))) d:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime d⊢ toTensor.symm ((permT id ⋯) ((contrT 2 1 2 ⋯) ((prodT (contrMetric d)) (toTensor (tensorDeriv A.val x))))) + -toTensor.symm ((permT (![1, 0] ∘ id) ⋯) ((contrT 2 1 2 ⋯) ((prodT (contrMetric d)) (toTensor (tensorDeriv A.val x))))) = toTensor.symm ((permT id ⋯) ((contrT 2 1 2 ⋯) ((prodT (contrMetric d)) (toTensor (tensorDeriv A.val x))))) + -toTensor.symm ((permT ![1, 0] ⋯) ((contrT 2 1 2 ⋯) ((prodT (contrMetric d)) (toTensor (tensorDeriv A.val x))))) All goals completed! 🐙lemma toTensor_toFieldStrength {d} (A : ElectromagneticPotential d) (x : SpaceTime d) : Tensorial.toTensor (toFieldStrength A x) = (permT id (IsReindexing.auto) {(η d | μ μ' ⊗ A.deriv x | μ' ν)}ᵀ) - (permT ![1, 0] (IsReindexing.auto) {(η d | μ μ' ⊗ A.deriv x | μ' ν)}ᵀ) := d:ℕA:ElectromagneticPotential dx:SpaceTime d⊢ toTensor (A.toFieldStrength x) = (permT id ⋯) ((contrT 2 1 2 ⋯) ((prodT (contrMetric d)) (toTensor (A.deriv x)))) - (permT ![1, 0] ⋯) ((contrT 2 1 2 ⋯) ((prodT (contrMetric d)) (toTensor (A.deriv x)))) All goals completed! 🐙

A.2. Vector equalities

These equalities for the field strength tensor are in terms of vector basis. They match some of the familiar forms one might expect to see the field strength tensor in.

The statement that F = F^{μν} eᵤ ⊗ eᵥ written explicitly, with the components extracted via toField.

lemma toFieldStrength_eq_sum_basis_eval {d} {A : ElectromagneticPotential d} : A.toFieldStrength = fun x => ∑ μ, ∑ ν, toField {A.toFieldStrength x| [μ] [ν]}ᵀ • Vector.basis μ ⊗ₜ[ℝ] Vector.basis ν := d:ℕA:ElectromagneticPotential d⊢ A.toFieldStrength = fun x => ∑ μ, ∑ ν, toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (A.toFieldStrength x)))) • Vector.basis μ ⊗ₜ[ℝ] Vector.basis ν d:ℕA:ElectromagneticPotential dx:SpaceTime d⊢ A.toFieldStrength x = ∑ μ, ∑ ν, toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (A.toFieldStrength x)))) • Vector.basis μ ⊗ₜ[ℝ] Vector.basis ν All goals completed! 🐙

The statement that F = F^{μν} eᵤ ⊗ eᵥ written explicitly, with the components given by ∑ κ, (η μ κ * ∂_ κ A x ν - η ν κ * ∂_ κ A x μ).

lemma toFieldStrength_eq_sum_basis {d} {A : ElectromagneticPotential d} (hA : Differentiable ℝ A) (x : SpaceTime d) : A.toFieldStrength x = ∑ μ, ∑ ν, (∑ κ, (η μ κ * ∂_ κ A x ν - η ν κ * ∂_ κ A x μ)) • Lorentz.Vector.basis μ ⊗ₜ Lorentz.Vector.basis ν := d:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime d⊢ A.toFieldStrength x = ∑ μ, ∑ ν, (∑ κ, (η μ κ * ∂_ κ A.val x ν - η ν κ * ∂_ κ A.val x μ)) • Vector.basis μ ⊗ₜ[ℝ] Vector.basis ν d:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime d⊢ (Vector.basis.tensorProduct Vector.basis).repr (A.toFieldStrength x) = (Vector.basis.tensorProduct Vector.basis).repr (∑ μ, ∑ ν, (∑ κ, (η μ κ * ∂_ κ A.val x ν - η ν κ * ∂_ κ A.val x μ)) • Vector.basis μ ⊗ₜ[ℝ] Vector.basis ν) d:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ((Vector.basis.tensorProduct Vector.basis).repr (A.toFieldStrength x)) (μ, ν) = ((Vector.basis.tensorProduct Vector.basis).repr (∑ μ, ∑ ν, (∑ κ, (η μ κ * ∂_ κ A.val x ν - η ν κ * ∂_ κ A.val x μ)) • Vector.basis μ ⊗ₜ[ℝ] Vector.basis ν)) (μ, ν) d:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ((Vector.basis.tensorProduct Vector.basis).repr (A.toFieldStrength x)) (μ, ν) = ∑ κ, (η μ κ * ∂_ κ A.val x ν - η ν κ * ∂_ κ A.val x μ) d:ℕA:ElectromagneticPotential dhA:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ∑ x_1, η ((ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i => (basisIdxCongr ⋯) ((ComponentIdx.prod.trans (Vector.indexEquiv.prodCongr Vector.indexEquiv)).symm (μ, ν) (IsReindexing.inv id ⋯ i))) (x_1, x_1))).1 0) ((ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i => (basisIdxCongr ⋯) ((ComponentIdx.prod.trans (Vector.indexEquiv.prodCongr Vector.indexEquiv)).symm (μ, ν) (IsReindexing.inv id ⋯ i))) (x_1, x_1))).1 1) * ∂_ ((ComponentIdx.prod.trans (CoVector.indexEquiv.prodCongr Vector.indexEquiv)) (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i => (basisIdxCongr ⋯) ((ComponentIdx.prod.trans (Vector.indexEquiv.prodCongr Vector.indexEquiv)).symm (μ, ν) (IsReindexing.inv id ⋯ i))) (x_1, x_1))).2).1 A.val x ((ComponentIdx.prod.trans (CoVector.indexEquiv.prodCongr Vector.indexEquiv)) (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i => (basisIdxCongr ⋯) ((ComponentIdx.prod.trans (Vector.indexEquiv.prodCongr Vector.indexEquiv)).symm (μ, ν) (IsReindexing.inv id ⋯ i))) (x_1, x_1))).2).2 - ∑ x_1, η ((ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i => (basisIdxCongr ⋯) ((ComponentIdx.prod.trans (Vector.indexEquiv.prodCongr Vector.indexEquiv)).symm (μ, ν) (IsReindexing.inv ![1, 0] ⋯ i))) (x_1, x_1))).1 0) ((ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i => (basisIdxCongr ⋯) ((ComponentIdx.prod.trans (Vector.indexEquiv.prodCongr Vector.indexEquiv)).symm (μ, ν) (IsReindexing.inv ![1, 0] ⋯ i))) (x_1, x_1))).1 1) * ∂_ ((ComponentIdx.prod.trans (CoVector.indexEquiv.prodCongr Vector.indexEquiv)) (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i => (basisIdxCongr ⋯) ((ComponentIdx.prod.trans (Vector.indexEquiv.prodCongr Vector.indexEquiv)).symm (μ, ν) (IsReindexing.inv ![1, 0] ⋯ i))) (x_1, x_1))).2).1 A.val x ((ComponentIdx.prod.trans (CoVector.indexEquiv.prodCongr Vector.indexEquiv)) (ComponentIdx.prod ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ fun i => (basisIdxCongr ⋯) ((ComponentIdx.prod.trans (Vector.indexEquiv.prodCongr Vector.indexEquiv)).symm (μ, ν) (IsReindexing.inv ![1, 0] ⋯ i))) (x_1, x_1))).2).2 = ∑ x_1, η μ x_1 * ∂_ x_1 A.val x ν - ∑ x_1, η ν x_1 * ∂_ x_1 A.val x μ All goals completed! 🐙

The statement that F = F^{μν} eᵤ ⊗ eᵥ written explicitly, with with the components given by (η μ μ * ∂_ μ A x ν - η ν ν * ∂_ ν A x μ).

All goals completed! 🐙

A.3. The group action acting on the field strength tensor

We show that the field strength tensor is equivariant under the action of the Lorentz group. That is transforming the potential and then taking the field strength is the same as taking the field strength and then transforming the resulting tensor.

d:ℕA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.valx:SpaceTime d⊢ toTensor.symm ((permT id toFieldStrength._proof_3) ((contrT 2 1 2 ⋯) ((prodT (Λ • contrMetric d)) (toTensor (Λ • A.deriv (Λ⁻¹ • x)))) + (permT ![1, 0] toFieldStrength._proof_7) (-(contrT 2 1 2 ⋯) ((prodT (Λ • contrMetric d)) (toTensor (Λ • A.deriv (Λ⁻¹ • x))))))) = Λ • toTensor.symm ((permT id toFieldStrength._proof_3) ((contrT 2 1 2 ⋯) ((prodT (contrMetric d)) (toTensor (A.deriv (Λ⁻¹ • x)))) + (permT ![1, 0] toFieldStrength._proof_7) (-(contrT 2 1 2 ⋯) ((prodT (contrMetric d)) (toTensor (A.deriv (Λ⁻¹ • x))))))) All goals completed! 🐙

This lemma expresses the component form of the transformed field strength tensor: when a Lorentz transformation Λ acts on the potential A, the resulting field strength tensor's components are given by the standard tensor transformation rule involving the Lorentz matrix elements Λ^μ_κ and Λ^ν_ρ applied to the original field components.

d:ℕA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.valx:SpaceTime dν:Fin 1 ⊕ Fin dx✝:ν ∈ Finset.univ⊢ ∑ y, ∑ x_1, ∑ x_2, (toField ((evalT 0 x_2) ((evalT 0 x_1) (toTensor (A.toFieldStrength (Λ⁻¹ • x))))) * (↑Λ y x_2 * ↑Λ ν x_1)) • Vector.basis ν ⊗ₜ[ℝ] Vector.basis y = ∑ x_1, (∑ x_2, ∑ x_3, ↑Λ ν x_2 * ↑Λ x_1 x_3 * toField ((evalT 0 x_3) ((evalT 0 x_2) (toTensor (A.toFieldStrength (Λ⁻¹ • x)))))) • Vector.basis ν ⊗ₜ[ℝ] Vector.basis x_1 d:ℕA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.valx:SpaceTime dν:Fin 1 ⊕ Fin dx✝¹:ν ∈ Finset.univμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ⊢ ∑ x_1, ∑ x_2, (toField ((evalT 0 x_2) ((evalT 0 x_1) (toTensor (A.toFieldStrength (Λ⁻¹ • x))))) * (↑Λ μ x_2 * ↑Λ ν x_1)) • Vector.basis ν ⊗ₜ[ℝ] Vector.basis μ = (∑ x_1, ∑ x_2, ↑Λ ν x_1 * ↑Λ μ x_2 * toField ((evalT 0 x_2) ((evalT 0 x_1) (toTensor (A.toFieldStrength (Λ⁻¹ • x)))))) • Vector.basis ν ⊗ₜ[ℝ] Vector.basis μ d:ℕA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.valx:SpaceTime dν:Fin 1 ⊕ Fin dx✝¹:ν ∈ Finset.univμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ⊢ (∑ i, ∑ i_1, toField ((evalT 0 i_1) ((evalT 0 i) (toTensor (A.toFieldStrength (Λ⁻¹ • x))))) * (↑Λ μ i_1 * ↑Λ ν i)) • Vector.basis ν ⊗ₜ[ℝ] Vector.basis μ = (∑ x_1, ∑ x_2, ↑Λ ν x_1 * ↑Λ μ x_2 * toField ((evalT 0 x_2) ((evalT 0 x_1) (toTensor (A.toFieldStrength (Λ⁻¹ • x)))))) • Vector.basis ν ⊗ₜ[ℝ] Vector.basis μ d:ℕA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.valx:SpaceTime dν:Fin 1 ⊕ Fin dx✝¹:ν ∈ Finset.univμ:Fin 1 ⊕ Fin dx✝:μ ∈ Finset.univ⊢ ∑ i, ∑ i_1, toField ((evalT 0 i_1) ((evalT 0 i) (toTensor (A.toFieldStrength (Λ⁻¹ • x))))) * (↑Λ μ i_1 * ↑Λ ν i) = ∑ x_1, ∑ x_2, ↑Λ ν x_1 * ↑Λ μ x_2 * toField ((evalT 0 x_2) ((evalT 0 x_1) (toTensor (A.toFieldStrength (Λ⁻¹ • x))))) exact Finset.sum_congr rfl (fun κ _ => Finset.sum_congr rfl (fun κ _ => d:ℕA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.valx:SpaceTime dν:Fin 1 ⊕ Fin dx✝³:ν ∈ Finset.univμ:Fin 1 ⊕ Fin dx✝²:μ ∈ Finset.univκ✝:Fin 1 ⊕ Fin dx✝¹:κ✝ ∈ Finset.univκ:Fin 1 ⊕ Fin dx✝:κ ∈ Finset.univ⊢ toField ((evalT 0 κ) ((evalT 0 κ✝) (toTensor (A.toFieldStrength (Λ⁻¹ • x))))) * (↑Λ μ κ * ↑Λ ν κ✝) = ↑Λ ν κ✝ * ↑Λ μ κ * toField ((evalT 0 κ) ((evalT 0 κ✝) (toTensor (A.toFieldStrength (Λ⁻¹ • x))))) All goals completed! 🐙))

A.4. Differentiability and smoothness of the field strength tensor

@[fun_prop] lemma differentiable_toFieldStrength {d} {A : ElectromagneticPotential d} (hA : ContDiff ℝ 2 A) : Differentiable ℝ A.toFieldStrength := d:ℕA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.val⊢ Differentiable ℝ A.toFieldStrength d:ℕA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.val⊢ Differentiable ℝ fun x => A.toFieldStrength x d:ℕA:ElectromagneticPotential dhA:ContDiff ℝ 2 A.val⊢ Differentiable ℝ fun x => ∑ μ, ∑ ν, (η μ μ * ∂_ μ A.val x ν - η ν ν * ∂_ ν A.val x μ) • Vector.basis μ ⊗ₜ[ℝ] Vector.basis ν All goals completed! 🐙@[fun_prop] lemma differentiable_toFieldStrength_of_smooth {d} {A : ElectromagneticPotential d} (hA : ContDiff ℝ ∞ A) : Differentiable ℝ A.toFieldStrength := differentiable_toFieldStrength (hA.of_le (ENat.LEInfty.out))@[fun_prop] lemma contDiff_toFieldStrength {d} {n : WithTop ℕ∞} {A : ElectromagneticPotential d} (hA : ContDiff ℝ (n + 1) A) : ContDiff ℝ n A.toFieldStrength := d:ℕn:ℕ∞ωA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.val⊢ ContDiff ℝ n A.toFieldStrength d:ℕn:ℕ∞ωA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.val⊢ ContDiff ℝ n fun x => A.toFieldStrength x d:ℕn:ℕ∞ωA:ElectromagneticPotential dhA:ContDiff ℝ (n + 1) A.val⊢ ContDiff ℝ n fun x => ∑ μ, ∑ ν, (η μ μ * ∂_ μ A.val x ν - η ν ν * ∂_ ν A.val x μ) • Vector.basis μ ⊗ₜ[ℝ] Vector.basis ν All goals completed! 🐙

A.5. Elements of the field strength tensor in terms of basis

TODO "For the electromagnetic field strength, we have lots of lemmas related to the components of the field strength tensor in terms of the basis. For example, `toTensor_toFieldStrength_basis_repr`, these should be removed. They are used downstream, so there use there should be refactored."All goals completed! 🐙d:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.up] ![Color.up])hb:(Vector.basis.reindex Vector.indexEquiv.symm).tensorProduct (Vector.basis.reindex Vector.indexEquiv.symm) = (Vector.basis.tensorProduct Vector.basis).reindex (Vector.indexEquiv.symm.prodCongr Vector.indexEquiv.symm)⊢ ((Vector.basis.tensorProduct Vector.basis).repr (A.toFieldStrength x)) ((Vector.indexEquiv.symm.prodCongr Vector.indexEquiv.symm).symm (ComponentIdx.prod b)) = ((Vector.basis.tensorProduct Vector.basis).repr (A.toFieldStrength x)) (b 0, b 1) All goals completed! 🐙d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ((CoVector.basis.tensorProduct Vector.basis).repr (A.toFieldStrength x)) (μ, ν) = ((Vector.basis.tensorProduct Vector.basis).repr (A.toFieldStrength x)) (match 0 with | 0 => μ | 1 => ν, match 1 with | 0 => μ | 1 => ν) All goals completed! 🐙All goals completed! 🐙
A.5.1. Index evaluation

These lemmas express the components of the field strength tensor using index evaluation.

Evaluating both tensor indices of the field strength gives the coefficient in the standard tensor-product basis.

lemma toFieldStrength_eval_eq_basis_repr {d} (A : ElectromagneticPotential d) (x : SpaceTime d) (μ ν : Fin 1 ⊕ Fin d) : toField {A.toFieldStrength x | [μ] [ν]}ᵀ = (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x) (μ, ν) := d:ℕA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (A.toFieldStrength x)))) = ((CoVector.basis.tensorProduct Vector.basis).repr (A.toFieldStrength x)) (μ, ν) d:ℕA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (A.toFieldStrength x)))) = ((Vector.basis.tensorProduct Vector.basis).repr (A.toFieldStrength x)) (μ, ν)d:ℕA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ((Vector.basis.tensorProduct Vector.basis).repr (A.toFieldStrength x)) (μ, ν) = ((CoVector.basis.tensorProduct Vector.basis).repr (A.toFieldStrength x)) (μ, ν) d:ℕA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ toField ((evalT 0 ν) ((evalT 0 μ) (toTensor (A.toFieldStrength x)))) = ((Vector.basis.tensorProduct Vector.basis).repr (A.toFieldStrength x)) (μ, ν) conv_rhs => d:ℕA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d| ((Vector.basis.tensorProduct Vector.basis).repr (∑ i, ∑ j, toField ((evalT 0 ((basisIdxCongr ⋯) j)) ((evalT 0 ((basisIdxCongr ⋯) i)) (toTensor (A.toFieldStrength x)))) • Vector.basis i ⊗ₜ[ℝ] Vector.basis j)) (μ, ν) All goals completed! 🐙 d:ℕA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ((Vector.basis.tensorProduct Vector.basis).repr (A.toFieldStrength x)) (μ, ν) = ((CoVector.basis.tensorProduct Vector.basis).repr (A.toFieldStrength x)) (μ, ν) All goals completed! 🐙

The evaluated components of the field strength tensor in terms of derivatives of the electromagnetic potential.

d:ℕA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ((CoVector.basis.tensorProduct Vector.basis).repr (A.toFieldStrength x)) (μ, ν) = ∑ κ, (η μ κ * ∂_ κ A.val x ν - η ν κ * ∂_ κ A.val x μ) All goals completed! 🐙

The evaluated components of the field strength tensor after using diagonal form of the Minkowski metric.

d:ℕA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ((CoVector.basis.tensorProduct Vector.basis).repr (A.toFieldStrength x)) (μ, ν) = η μ μ * ∂_ μ A.val x ν - η ν ν * ∂_ ν A.val x μ All goals completed! 🐙

A.6. The field strength matrix

We define the field strength matrix to be the matrix representation of the field strength tensor in the standard basis.

This is currently not used as much as it could be.

lemma fieldStrengthMatrix_eq {d} (A : ElectromagneticPotential d) (x : SpaceTime d) : A.fieldStrengthMatrix x = (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x) := d:ℕA:ElectromagneticPotential dx:SpaceTime d⊢ A.fieldStrengthMatrix x = (CoVector.basis.tensorProduct Vector.basis).repr (A.toFieldStrength x) All goals completed! 🐙

Index evaluation of the field strength tensor agrees with the corresponding component of the field strength matrix.

All goals completed! 🐙
d:ℕA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ (A.fieldStrengthMatrix x) (μ, ν) = ((Vector.basis.tensorProduct Vector.basis).repr (A.toFieldStrength x)) (match 0 with | 0 => μ | 1 => ν, match 1 with | 0 => μ | 1 => ν) All goals completed! 🐙lemma toFieldStrength_eq_fieldStrengthMatrix {d} (A : ElectromagneticPotential d) : toFieldStrength A = fun x => ∑ μ, ∑ ν, A.fieldStrengthMatrix x (μ, ν) • (Lorentz.Vector.basis μ) ⊗ₜ (Lorentz.Vector.basis ν) := d:ℕA:ElectromagneticPotential d⊢ A.toFieldStrength = fun x => ∑ μ, ∑ ν, (A.fieldStrengthMatrix x) (μ, ν) • Vector.basis μ ⊗ₜ[ℝ] Vector.basis ν d:ℕA:ElectromagneticPotential dx:SpaceTime d⊢ A.toFieldStrength x = ∑ μ, ∑ ν, (A.fieldStrengthMatrix x) (μ, ν) • Vector.basis μ ⊗ₜ[ℝ] Vector.basis ν d:ℕA:ElectromagneticPotential dx:SpaceTime d⊢ (Vector.basis.tensorProduct Vector.basis).repr (A.toFieldStrength x) = (Vector.basis.tensorProduct Vector.basis).repr (∑ μ, ∑ ν, (A.fieldStrengthMatrix x) (μ, ν) • Vector.basis μ ⊗ₜ[ℝ] Vector.basis ν) d:ℕA:ElectromagneticPotential dx:SpaceTime d⊢ (Vector.basis.tensorProduct Vector.basis).repr (A.toFieldStrength x) = ∑ x_1, ∑ x_2, (A.fieldStrengthMatrix x) (x_1, x_2) • (Vector.basis.tensorProduct Vector.basis).repr (Vector.basis x_1 ⊗ₜ[ℝ] Vector.basis x_2) d:ℕA:ElectromagneticPotential dx:SpaceTime dκ:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)⊢ ((Vector.basis.tensorProduct Vector.basis).repr (A.toFieldStrength x)) κ = (∑ x_1, ∑ x_2, (A.fieldStrengthMatrix x) (x_1, x_2) • (Vector.basis.tensorProduct Vector.basis).repr (Vector.basis x_1 ⊗ₜ[ℝ] Vector.basis x_2)) κ match κ with d:ℕA:ElectromagneticPotential dx:SpaceTime dκ:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)μ':Fin 1 ⊕ Fin dν':Fin 1 ⊕ Fin d⊢ ((Vector.basis.tensorProduct Vector.basis).repr (A.toFieldStrength x)) (μ', ν') = (∑ x_1, ∑ x_2, (A.fieldStrengthMatrix x) (x_1, x_2) • (Vector.basis.tensorProduct Vector.basis).repr (Vector.basis x_1 ⊗ₜ[ℝ] Vector.basis x_2)) (μ', ν') d:ℕA:ElectromagneticPotential dx:SpaceTime dκ:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)μ':Fin 1 ⊕ Fin dν':Fin 1 ⊕ Fin d⊢ ((Vector.basis.tensorProduct Vector.basis).repr (A.toFieldStrength x)) (μ', ν') = (A.fieldStrengthMatrix x) (μ', ν') All goals completed! 🐙
A.6.1. Differentiability of the field strength matrix
d:ℕA:ElectromagneticPotential dμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)hA:ContDiff ℝ 2 A.valdiff_partial:∀ (μ ν : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => (fderiv ℝ A.val x) (Vector.basis μ) ν⊢ Differentiable ℝ fun x => (A.fieldStrengthMatrix x) μν d:ℕA:ElectromagneticPotential dμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)hA:ContDiff ℝ 2 A.valdiff_partial:∀ (μ ν : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => (fderiv ℝ A.val x) (Vector.basis μ) ν| Differentiable ℝ fun x => (A.fieldStrengthMatrix x) μν d:ℕA:ElectromagneticPotential dμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)hA:ContDiff ℝ 2 A.valdiff_partial:∀ (μ ν : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => (fderiv ℝ A.val x) (Vector.basis μ) νx:SpaceTime d| (A.fieldStrengthMatrix x) μν; d:ℕA:ElectromagneticPotential dμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)hA:ContDiff ℝ 2 A.valdiff_partial:∀ (μ ν : Fin 1 ⊕ Fin d), Differentiable ℝ fun x => (fderiv ℝ A.val x) (Vector.basis μ) νx:SpaceTime d| η μν.1 μν.1 * (fderiv ℝ A.val x) (Vector.basis μν.1) μν.2 - η μν.2 μν.2 * (fderiv ℝ A.val x) (Vector.basis μν.2) μν.1 All goals completed! 🐙lemma fieldStrengthMatrix_differentiable_space {d} {A : ElectromagneticPotential d} {μν} (hA : ContDiff ℝ 2 A) (t : Time) {c : SpeedOfLight} : Differentiable ℝ (fun x => A.fieldStrengthMatrix ((toTimeAndSpace c).symm (t, x)) μν) := d:ℕA:ElectromagneticPotential dμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)hA:ContDiff ℝ 2 A.valt:Timec:SpeedOfLight⊢ Differentiable ℝ fun x => (A.fieldStrengthMatrix ((toTimeAndSpace c).symm (t, x))) μν d:ℕA:ElectromagneticPotential dμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)hA:ContDiff ℝ 2 A.valt:Timec:SpeedOfLight⊢ Differentiable ℝ ((fun x => (A.fieldStrengthMatrix x) μν) ∘ fun x => (toTimeAndSpace c).symm (t, x)) exact (fieldStrengthMatrix_differentiable hA).comp (d:ℕA:ElectromagneticPotential dμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)hA:ContDiff ℝ 2 A.valt:Timec:SpeedOfLight⊢ Differentiable ℝ fun x => (toTimeAndSpace c).symm (t, x) All goals completed! 🐙)lemma fieldStrengthMatrix_differentiable_time {d} {A : ElectromagneticPotential d} {μν} (hA : ContDiff ℝ 2 A) (x : Space d) {c : SpeedOfLight} : Differentiable ℝ (fun t => A.fieldStrengthMatrix ((toTimeAndSpace c).symm (t, x)) μν) := d:ℕA:ElectromagneticPotential dμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)hA:ContDiff ℝ 2 A.valx:Space dc:SpeedOfLight⊢ Differentiable ℝ fun t => (A.fieldStrengthMatrix ((toTimeAndSpace c).symm (t, x))) μν d:ℕA:ElectromagneticPotential dμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)hA:ContDiff ℝ 2 A.valx:Space dc:SpeedOfLight⊢ Differentiable ℝ ((fun x => (A.fieldStrengthMatrix x) μν) ∘ fun t => (toTimeAndSpace c).symm (t, x)) exact (fieldStrengthMatrix_differentiable hA).comp (d:ℕA:ElectromagneticPotential dμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)hA:ContDiff ℝ 2 A.valx:Space dc:SpeedOfLight⊢ Differentiable ℝ fun t => (toTimeAndSpace c).symm (t, x) All goals completed! 🐙)d:ℕn:ℕ∞ωA:ElectromagneticPotential dμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)hA:ContDiff ℝ (n + 1) A.valν:Fin 1 ⊕ Fin d⊢ ContDiff ℝ n fun x => (fderiv ℝ A.val x) (Vector.basis ν) exact ContDiff.clm_apply (ContDiff.fderiv_right (m := n) hA (d:ℕn:ℕ∞ωA:ElectromagneticPotential dμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)hA:ContDiff ℝ (n + 1) A.valν:Fin 1 ⊕ Fin d⊢ n + 1 ≤ n + 1 All goals completed! 🐙)) (d:ℕn:ℕ∞ωA:ElectromagneticPotential dμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)hA:ContDiff ℝ (n + 1) A.valν:Fin 1 ⊕ Fin d⊢ ContDiff ℝ n fun x => Vector.basis ν All goals completed! 🐙)lemma fieldStrengthMatrix_smooth {d} {A : ElectromagneticPotential d} (hA : ContDiff ℝ ∞ A) (μν) : ContDiff ℝ ∞ (A.fieldStrengthMatrix · μν) := fieldStrengthMatrix_contDiff (d:ℕA:ElectromagneticPotential dhA:ContDiff ℝ ∞ A.valμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)⊢ ContDiff ℝ (∞ + 1) A.val All goals completed! 🐙)

A.7. The antisymmetry of the field strength tensor

We show that the field strength tensor is antisymmetric.

d:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.up] ![Color.up])⊢ ∑ κ, (η (b 0) κ * ∂_ κ A.val x (b 1) - η (b 1) κ * ∂_ κ A.val x (b 0)) = ∑ x_1, -(η ((basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ 0))) x_1 * ∂_ x_1 A.val x ((basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ 1))) - η ((basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ 1))) x_1 * ∂_ x_1 A.val x ((basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ 0)))) d:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.up] ![Color.up])κ:Fin 1 ⊕ Fin dx✝:κ ∈ Finset.univ⊢ η (b 0) κ * ∂_ κ A.val x (b 1) - η (b 1) κ * ∂_ κ A.val x (b 0) = -(η ((basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ 0))) κ * ∂_ κ A.val x ((basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ 1))) - η ((basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ 1))) κ * ∂_ κ A.val x ((basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ 0)))) d:ℕA:ElectromagneticPotential dx:SpaceTime db:ComponentIdx (Fin.append ![Color.up] ![Color.up])κ:Fin 1 ⊕ Fin dx✝:κ ∈ Finset.univ⊢ η (b 0) κ * ∂_ κ A.val x (b 1) - η (b 1) κ * ∂_ κ A.val x (b 0) = η ((basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ 1))) κ * ∂_ κ A.val x ((basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ 0))) - η ((basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ 0))) κ * ∂_ κ A.val x ((basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0] ⋯ 1))) All goals completed! 🐙d:ℕA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ∑ κ, (η (μ, ν).1 κ * ∂_ κ A.val x (μ, ν).2 - η (μ, ν).2 κ * ∂_ κ A.val x (μ, ν).1) = ∑ x_1, -(η (ν, μ).1 x_1 * ∂_ x_1 A.val x (ν, μ).2 - η (ν, μ).2 x_1 * ∂_ x_1 A.val x (ν, μ).1) exact Finset.sum_congr rfl fun κ _ => d:ℕA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dκ:Fin 1 ⊕ Fin dx✝:κ ∈ Finset.univ⊢ η (μ, ν).1 κ * ∂_ κ A.val x (μ, ν).2 - η (μ, ν).2 κ * ∂_ κ A.val x (μ, ν).1 = -(η (ν, μ).1 κ * ∂_ κ A.val x (ν, μ).2 - η (ν, μ).2 κ * ∂_ κ A.val x (ν, μ).1) All goals completed! 🐙@[simp] lemma fieldStrengthMatrix_diag_eq_zero {d} (A : ElectromagneticPotential d) (x : SpaceTime d) (μ : Fin 1 ⊕ Fin d) : A.fieldStrengthMatrix x (μ, μ) = 0 := d:ℕA:ElectromagneticPotential dx:SpaceTime dμ:Fin 1 ⊕ Fin d⊢ (A.fieldStrengthMatrix x) (μ, μ) = 0 All goals completed! 🐙

A.8. Equivariance of the field strength matrix

d:ℕA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dF:Lorentz.Vector d ⊗[ℝ] Lorentz.Vector dP:Lorentz.Vector d ⊗[ℝ] Lorentz.Vector d → Prop := fun F => ((CoVector.basis.tensorProduct Vector.basis).repr (Λ • F)) (μ, ν) = ∑ κ, ∑ ρ, ↑Λ μ κ * ↑Λ ν ρ * ((CoVector.basis.tensorProduct Vector.basis).repr F) (κ, ρ)F1:Lorentz.Vector d ⊗[ℝ] Lorentz.Vector dF2:Lorentz.Vector d ⊗[ℝ] Lorentz.Vector dh1:P F1h2:P F2κ:Fin 1 ⊕ Fin dx✝:κ ∈ Finset.univ⊢ ∑ x, (↑Λ μ κ * ↑Λ ν x * ((CoVector.basis.tensorProduct Vector.basis).repr F1) (κ, x) + ↑Λ μ κ * ↑Λ ν x * ((CoVector.basis.tensorProduct Vector.basis).repr F2) (κ, x)) = ∑ x, ↑Λ μ κ * ↑Λ ν x * (((CoVector.basis.tensorProduct Vector.basis).repr F1) (κ, x) + ((CoVector.basis.tensorProduct Vector.basis).repr F2) (κ, x)) exact Finset.sum_congr rfl fun ρ _ => d:ℕA:ElectromagneticPotential dΛ:↑(LorentzGroup d)hf:Differentiable ℝ A.valx:SpaceTime dμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dF:Lorentz.Vector d ⊗[ℝ] Lorentz.Vector dP:Lorentz.Vector d ⊗[ℝ] Lorentz.Vector d → Prop := fun F => ((CoVector.basis.tensorProduct Vector.basis).repr (Λ • F)) (μ, ν) = ∑ κ, ∑ ρ, ↑Λ μ κ * ↑Λ ν ρ * ((CoVector.basis.tensorProduct Vector.basis).repr F) (κ, ρ)F1:Lorentz.Vector d ⊗[ℝ] Lorentz.Vector dF2:Lorentz.Vector d ⊗[ℝ] Lorentz.Vector dh1:P F1h2:P F2κ:Fin 1 ⊕ Fin dx✝¹:κ ∈ Finset.univρ:Fin 1 ⊕ Fin dx✝:ρ ∈ Finset.univ⊢ ↑Λ μ κ * ↑Λ ν ρ * ((CoVector.basis.tensorProduct Vector.basis).repr F1) (κ, ρ) + ↑Λ μ κ * ↑Λ ν ρ * ((CoVector.basis.tensorProduct Vector.basis).repr F2) (κ, ρ) = ↑Λ μ κ * ↑Λ ν ρ * (((CoVector.basis.tensorProduct Vector.basis).repr F1) (κ, ρ) + ((CoVector.basis.tensorProduct Vector.basis).repr F2) (κ, ρ)) All goals completed! 🐙

A.9. Linearity of the field strength tensor

We show that the field strength tensor is linear in the potential.

d:ℕA1:ElectromagneticPotential dA2:ElectromagneticPotential dx:SpaceTime dhA1:Differentiable ℝ A1.valhA2:Differentiable ℝ A2.valμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)κ:Fin 1 ⊕ Fin dx✝:κ ∈ Finset.univ⊢ η μν.1 κ * (fderiv ℝ A1.val x + fderiv ℝ A2.val x) (Vector.basis κ) μν.2 - η μν.2 κ * (fderiv ℝ A1.val x + fderiv ℝ A2.val x) (Vector.basis κ) μν.1 = η μν.1 κ * (fderiv ℝ A1.val x) (Vector.basis κ) μν.2 - η μν.2 κ * (fderiv ℝ A1.val x) (Vector.basis κ) μν.1 + (η μν.1 κ * (fderiv ℝ A2.val x) (Vector.basis κ) μν.2 - η μν.2 κ * (fderiv ℝ A2.val x) (Vector.basis κ) μν.1) d:ℕA1:ElectromagneticPotential dA2:ElectromagneticPotential dx:SpaceTime dhA1:Differentiable ℝ A1.valhA2:Differentiable ℝ A2.valμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)κ:Fin 1 ⊕ Fin dx✝:κ ∈ Finset.univ⊢ η μν.1 κ * ((fderiv ℝ A1.val x) (Vector.basis κ) μν.2 + (fderiv ℝ A2.val x) (Vector.basis κ) μν.2) - η μν.2 κ * ((fderiv ℝ A1.val x) (Vector.basis κ) μν.1 + (fderiv ℝ A2.val x) (Vector.basis κ) μν.1) = η μν.1 κ * (fderiv ℝ A1.val x) (Vector.basis κ) μν.2 - η μν.2 κ * (fderiv ℝ A1.val x) (Vector.basis κ) μν.1 + (η μν.1 κ * (fderiv ℝ A2.val x) (Vector.basis κ) μν.2 - η μν.2 κ * (fderiv ℝ A2.val x) (Vector.basis κ) μν.1) All goals completed! 🐙set_option backward.isDefEq.respectTransparency false in lemma fieldStrengthMatrix_add {d} (A1 A2 : ElectromagneticPotential d) (x : SpaceTime d) (hA1 : Differentiable ℝ A1) (hA2 : Differentiable ℝ A2) : (A1 + A2).fieldStrengthMatrix x = A1.fieldStrengthMatrix x + A2.fieldStrengthMatrix x := d:ℕA1:ElectromagneticPotential dA2:ElectromagneticPotential dx:SpaceTime dhA1:Differentiable ℝ A1.valhA2:Differentiable ℝ A2.val⊢ (A1 + A2).fieldStrengthMatrix x = A1.fieldStrengthMatrix x + A2.fieldStrengthMatrix x All goals completed! 🐙d:ℕc:ℝA:ElectromagneticPotential dx:SpaceTime dhA:Differentiable ℝ A.valμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)κ:Fin 1 ⊕ Fin dx✝:κ ∈ Finset.univ⊢ η μν.1 κ * (c • fderiv ℝ A.val x) (Vector.basis κ) μν.2 - η μν.2 κ * (c • fderiv ℝ A.val x) (Vector.basis κ) μν.1 = c * (η μν.1 κ * (fderiv ℝ A.val x) (Vector.basis κ) μν.2 - η μν.2 κ * (fderiv ℝ A.val x) (Vector.basis κ) μν.1) d:ℕc:ℝA:ElectromagneticPotential dx:SpaceTime dhA:Differentiable ℝ A.valμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)κ:Fin 1 ⊕ Fin dx✝:κ ∈ Finset.univ⊢ η μν.1 κ * (c * (fderiv ℝ A.val x) (Vector.basis κ) μν.2) - η μν.2 κ * (c * (fderiv ℝ A.val x) (Vector.basis κ) μν.1) = c * (η μν.1 κ * (fderiv ℝ A.val x) (Vector.basis κ) μν.2 - η μν.2 κ * (fderiv ℝ A.val x) (Vector.basis κ) μν.1) All goals completed! 🐙set_option backward.isDefEq.respectTransparency false in lemma fieldStrengthMatrix_smul {d} (c : ℝ) (A : ElectromagneticPotential d) (x : SpaceTime d) (hA : Differentiable ℝ A) : (c • A).fieldStrengthMatrix x = c • A.fieldStrengthMatrix x := d:ℕc:ℝA:ElectromagneticPotential dx:SpaceTime dhA:Differentiable ℝ A.val⊢ (c • A).fieldStrengthMatrix x = c • A.fieldStrengthMatrix x All goals completed! 🐙