Merge pull request #419 from HEPLean/style-lint-changes

feat: Update todos

PhysLean/Electromagnetism/MaxwellEquations.lean

@@ -60,5 +60,8 @@ def MaxwellEquations (E : ElectricField) (B : MagneticField) : Prop :=
   𝓔.GaussLawElectric E ∧ GaussLawMagnetic B ∧
   FaradayLaw E B ∧ 𝓔.AmpereLaw E B
 
+TODO "Show that if the charge density is spherically symmetric,
+  then the electric field is also spherically symmetric."
+
 end EMSystem
 end Electromagnetism

PhysLean/Relativity/Lorentz/RealTensor/Derivative.lean

@@ -70,7 +70,9 @@ lemma derivative_repr {d n m : ℕ} {cm : Fin m → (realLorentzTensor d).C}
   · rw [← differentiableAt_pi]
     exact h1
 
-TODO "Prove that the derivative obeys the correct equivariant with respect to the
-  Lorentz group."
+TODO "Prove that the derivative obeys the following equivariant
+  property with respect to the Lorentz group.
+  For a function `f :  ℝT(d, cm) → ℝT(d, cn)` then
+  `Λ • (∂ f (x)) = ∂ (fun x => Λ • f (Λ⁻¹ • x)) (Λ • x)`."
 
 end realLorentzTensor