DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Update Basic.lean

Browse source
This commit is contained in:
Pietro Monticone 2024-08-20 14:04:52 +02:00
parent dce10c58df
commit 524831d32e
1 changed files with 4 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

13
HepLean/SpaceTime/Basic.lean
View file

@ -27,7 +27,6 @@ instance : Module ℝ SpaceTime := Pi.module _ _ _
instance euclideanNormedAddCommGroup : NormedAddCommGroup SpaceTime := Pi.normedAddCommGroup
instance euclideanNormedSpace : NormedSpace ℝ SpaceTime := Pi.normedSpace
namespace SpaceTime
open Manifold
@ -56,23 +55,19 @@ lemma stdBasis_not_eq {μ ν : Fin 4} (h : μ ≠ ν) : stdBasis μ ν = 0 := by
lemma stdBasis_0 : stdBasis 0 = ![1, 0, 0, 0] := by
funext i
fin_cases i
<;> simp [stdBasis_apply]
fin_cases i <;> simp [stdBasis_apply]
lemma stdBasis_1 : stdBasis 1 = ![0, 1, 0, 0] := by
funext i
fin_cases i
<;> simp [stdBasis_apply]
fin_cases i <;> simp [stdBasis_apply]
lemma stdBasis_2 : stdBasis 2 = ![0, 0, 1, 0] := by
funext i
fin_cases i
<;> simp [stdBasis_apply]
fin_cases i <;> simp [stdBasis_apply]
lemma stdBasis_3 : stdBasis 3 = ![0, 0, 0, 1] := by
funext i
fin_cases i
<;> simp [stdBasis_apply]
fin_cases i <;> simp [stdBasis_apply]
lemma stdBasis_mulVec (μ ν : Fin 4) (Λ : Matrix (Fin 4) (Fin 4) ℝ) :
(Λ *ᵥ stdBasis μ) ν = Λ ν μ := by