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

Docs: Add todos

Browse source
This commit is contained in:
jstoobysmith 2024-08-20 09:27:51 -04:00
parent b5428ac3e2
commit 01005ecd4c
3 changed files with 24 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
HepLean.lean
View file

@ -75,6 +75,7 @@ import HepLean.SpaceTime.LorentzTensor.Contraction
import HepLean.SpaceTime.LorentzTensor.EinsteinNotation.Basic
import HepLean.SpaceTime.LorentzTensor.EinsteinNotation.IndexNotation
import HepLean.SpaceTime.LorentzTensor.EinsteinNotation.Lemmas
import HepLean.SpaceTime.LorentzTensor.EinsteinNotation.RisingLowering
import HepLean.SpaceTime.LorentzTensor.IndexNotation.AreDual
import HepLean.SpaceTime.LorentzTensor.IndexNotation.Basic
import HepLean.SpaceTime.LorentzTensor.IndexNotation.Color

2
HepLean/SpaceTime/LorentzTensor/EinsteinNotation/Lemmas.lean
View file

@ -9,6 +9,8 @@ import HepLean.SpaceTime.LorentzTensor.EinsteinNotation.IndexNotation
# Lemmas regarding Einstein tensors
This file is currently a stub.
-/
namespace einsteinTensor

21
HepLean/SpaceTime/LorentzTensor/EinsteinNotation/RisingLowering.lean Normal file
View file

@ -0,0 +1,21 @@
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
import Mathlib.LinearAlgebra.StdBasis
import HepLean.SpaceTime.LorentzTensor.Basic
import Mathlib.LinearAlgebra.DirectSum.Finsupp
import Mathlib.LinearAlgebra.Finsupp
/-!
# Dualizing indices of Einstein tensors
Dualizing indices (the more general notion of rising and lowering indices) does
nothing for Einstein tensors, since they only have one color of index.
The aim of this file is show this result.
This file is currently a stub.
-/
/-! TODO: Prove dualizing indices for Einstein tensors does nothing. -/