Basis

📁 Source: PhysLean/Relativity/Tensors/Contraction/Basis.lean

Statistics

Metric	Count
Definitions DropPairSection, ofFin, ofFinEquiv, dropPair	4
Theorems mem_iff_apply_dropPairEmb_eq, mem_self_of_dropPair, ofFinEquiv_apply_fst, ofFinEquiv_apply_snd, ofFin_apply_fst, ofFin_apply_snd, ofFin_mem_dropPairEmbSection, dropPair_basisVector, contrT_basis_repr_apply, contrT_basis_repr_apply_eq_sum_fin	10
Total	14

TensorSpecies.Tensor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contrT_basis_repr_apply 📖	mathematical	TensorSpecies.τ	ComponentIdx Pure.dropPairEmb TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F basis contrT ComponentIdx.DropPairSection TensorSpecies.castToField IndexNotation.OverColor.Discrete.pairτ TensorSpecies.FD TensorSpecies.contr TensorSpecies.repDim TensorSpecies.basis	—	induction_on_basis basis_apply contrT_pure Pure.dropPair_basisVector basis_repr_pure Pure.component_basisVector TensorSpecies.basis_congr
contrT_basis_repr_apply_eq_sum_fin 📖	mathematical	TensorSpecies.τ	ComponentIdx Pure.dropPairEmb TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F basis contrT TensorSpecies.repDim ComponentIdx.DropPairSection ComponentIdx.DropPairSection.ofFinEquiv TensorSpecies.castToField IndexNotation.OverColor.Discrete.pairτ TensorSpecies.FD TensorSpecies.contr TensorSpecies.basis	—	contrT_basis_repr_apply ComponentIdx.DropPairSection.ofFinEquiv_apply_fst ComponentIdx.DropPairSection.ofFinEquiv_apply_snd

TensorSpecies.Tensor.ComponentIdx

Definitions

Name	Category	Theorems
DropPairSection 📖	CompOp	11 math math: complexLorentzTensor.contrT_ofRat_eq_sum_dropPairSection, DropPairSection.ofFin_mem_dropPairEmbSection, TensorSpecies.Tensor.contrT_basis_repr_apply_eq_sum_fin, complexLorentzTensor.contrT_ofRat, realLorentzTensor.contrT_basis_repr_apply_eq_dropPairSection, DropPairSection.ofFinEquiv_apply_fst, DropPairSection.ofFinEquiv_apply_snd, DropPairSection.mem_self_of_dropPair, TensorSpecies.Tensor.contrT_basis_repr_apply, realLorentzTensor.contrT_basis_repr_apply_eq_fin, DropPairSection.mem_iff_apply_dropPairEmb_eq
dropPair 📖	CompOp	1 math math: DropPairSection.mem_self_of_dropPair

TensorSpecies.Tensor.ComponentIdx.DropPairSection

Definitions

Name	Category	Theorems
ofFin 📖	CompOp	3 math math: ofFin_mem_dropPairEmbSection, ofFin_apply_snd, ofFin_apply_fst
ofFinEquiv 📖	CompOp	5 math math: TensorSpecies.Tensor.contrT_basis_repr_apply_eq_sum_fin, complexLorentzTensor.contrT_ofRat, ofFinEquiv_apply_fst, ofFinEquiv_apply_snd, realLorentzTensor.contrT_basis_repr_apply_eq_fin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_iff_apply_dropPairEmb_eq 📖	mathematical	—	TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.ComponentIdx.DropPairSection TensorSpecies.Tensor.Pure.dropPairEmb	—	—
mem_self_of_dropPair 📖	mathematical	—	TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.ComponentIdx.DropPairSection TensorSpecies.Tensor.ComponentIdx.dropPair	—	—
ofFinEquiv_apply_fst 📖	mathematical	—	TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.ComponentIdx.DropPairSection TensorSpecies.repDim ofFinEquiv	—	ofFin_apply_fst
ofFinEquiv_apply_snd 📖	mathematical	—	TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.ComponentIdx.DropPairSection TensorSpecies.repDim ofFinEquiv	—	ofFin_apply_snd
ofFin_apply_fst 📖	mathematical	—	ofFin TensorSpecies.repDim	—	—
ofFin_apply_snd 📖	mathematical	—	ofFin TensorSpecies.repDim	—	—
ofFin_mem_dropPairEmbSection 📖	mathematical	—	TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.ComponentIdx.DropPairSection ofFin	—	TensorSpecies.Tensor.Pure.dropPairEmbPre_dropPairEmb

TensorSpecies.Tensor.Pure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dropPair_basisVector 📖	mathematical	—	dropPair basisVector dropPairEmb	—	—

---

← Back to Index