Merge branch 'master' into Tensors

HepLean/SpaceTime/LorentzGroup/Basic.lean

@@ -151,7 +151,7 @@ lemma coe_inv : (Λ⁻¹).1 = Λ.1⁻¹:= by
   refine (inv_eq_left_inv ?h).symm
   exact mem_iff_dual_mul_self.mp Λ.2
 
-/-- The transpose of an matrix in the Lorentz group is an element of the Lorentz group. -/
+/-- The transpose of a matrix in the Lorentz group is an element of the Lorentz group. -/
 def transpose (Λ : LorentzGroup d) : LorentzGroup d :=
   ⟨Λ.1ᵀ, mem_iff_transpose.mp Λ.2⟩
 

HepLean/SpaceTime/LorentzVector/Basic.lean

@@ -22,7 +22,7 @@ variable (d : ℕ)
 /-- The type of Lorentz Vectors in `d`-space dimensions. -/
 def LorentzVector : Type := (Fin 1 ⊕ Fin d) → ℝ
 
-/-- An instance of a additive commutative monoid on `LorentzVector`. -/
+/-- An instance of an additive commutative monoid on `LorentzVector`. -/
 instance : AddCommMonoid (LorentzVector d) := Pi.addCommMonoid
 
 /-- An instance of a module on `LorentzVector`. -/

HepLean/SpaceTime/MinkowskiMetric.lean

@@ -23,7 +23,7 @@ open Matrix
 # The definition of the Minkowski Matrix
 
 -/
-/-- The `d.succ`-dimensional real of the form `diag(1, -1, -1, -1, ...)`. -/
+/-- The `d.succ`-dimensional real matrix of the form `diag(1, -1, -1, -1, ...)`. -/
 def minkowskiMatrix {d : ℕ} : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ :=
   LieAlgebra.Orthogonal.indefiniteDiagonal (Fin 1) (Fin d) ℝ
 
@@ -146,7 +146,7 @@ lemma self_eq_time_minus_norm : ⟪v, v⟫ₘ = v.time ^ 2 - ‖v.space‖ ^ 2 :
   rw [← real_inner_self_eq_norm_sq, PiLp.inner_apply, as_sum]
   noncomm_ring
 
-/-- The Minkowski metric is symmetric. -/
+/-- The Minkowski metric is symmetric in its arguments.. -/
 lemma symm : ⟪v, w⟫ₘ = ⟪w, v⟫ₘ := by
   simp only [as_sum]
   ac_rfl