ToComplex

📁 Source: PhysLean/Relativity/Tensors/RealTensor/ToComplex.lean

Statistics

Metric	Count
Definitions complexify, colorToComplex, evalIdxToComplex, evalTColorToComplex, prodTColorToComplex, toComplex	6
Theorems complexify_apply, complexify_comp_dropPairEmb, complexify_comp_succAbove, complexify_toFun_apply, colorToComplex_append, colorToComplex_comp_eq_match, colorToComplex_match_down, colorToComplex_match_up, complex_repDim_down, complex_repDim_up, complexify_prod, contrT_toComplex, evalT_toComplex, permCond_colorToComplex, permCond_prodTColorToComplex, permT_basis_complex, permT_basis_real, permT_toComplex, prodT_toComplex, tau_colorToComplex, toComplex_basis, toComplex_contrP_basisVector, toComplex_eq_sum_basis, toComplex_eq_zero_iff, toComplex_equivariant, toComplex_equivariant_slot_repr_down, toComplex_equivariant_slot_repr_up, toComplex_evalP_basisVector, toComplex_injective, toComplex_map_smul, toComplex_pure_basisVector, toComplex_repr	32
Total	38

TensorSpecies.Tensor.ComponentIdx

Definitions

Name	Category	Theorems
complexify 📖	CompOp	13 math math: realLorentzTensor.toComplex_evalP_basisVector, realLorentzTensor.complexify_prod, realLorentzTensor.ComponentIdx.complexify_apply, realLorentzTensor.toComplex_pure_basisVector, realLorentzTensor.toComplex_eq_sum_basis, realLorentzTensor.ComponentIdx.complexify_comp_dropPairEmb, realLorentzTensor.toComplex_equivariant_slot_repr_up, realLorentzTensor.toComplex_basis, realLorentzTensor.toComplex_contrP_basisVector, realLorentzTensor.ComponentIdx.complexify_comp_succAbove, realLorentzTensor.ComponentIdx.complexify_toFun_apply, realLorentzTensor.toComplex_repr, realLorentzTensor.toComplex_equivariant_slot_repr_down

realLorentzTensor

Definitions

Name	Category	Theorems
colorToComplex 📖	CompOp	26 math math: prodT_toComplex, tau_colorToComplex, toComplex_evalP_basisVector, complexify_prod, colorToComplex_comp_eq_match, toComplex_injective, contrT_toComplex, ComponentIdx.complexify_apply, toComplex_pure_basisVector, permCond_prodTColorToComplex, colorToComplex_append, toComplex_eq_sum_basis, permT_toComplex, evalT_toComplex, ComponentIdx.complexify_comp_dropPairEmb, toComplex_equivariant, toComplex_eq_zero_iff, toComplex_map_smul, toComplex_equivariant_slot_repr_up, toComplex_basis, toComplex_contrP_basisVector, ComponentIdx.complexify_comp_succAbove, permCond_colorToComplex, ComponentIdx.complexify_toFun_apply, toComplex_repr, toComplex_equivariant_slot_repr_down
evalIdxToComplex 📖	CompOp	1 math math: toComplex_evalP_basisVector
evalTColorToComplex 📖	CompOp	1 math math: evalT_toComplex
prodTColorToComplex 📖	CompOp	1 math math: prodT_toComplex
toComplex 📖	CompOp	14 math math: prodT_toComplex, toComplex_evalP_basisVector, toComplex_injective, contrT_toComplex, toComplex_pure_basisVector, toComplex_eq_sum_basis, permT_toComplex, evalT_toComplex, toComplex_equivariant, toComplex_eq_zero_iff, toComplex_map_smul, toComplex_basis, toComplex_contrP_basisVector, toComplex_repr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
colorToComplex_append 📖	mathematical	—	Color complexLorentzTensor.Color colorToComplex	—	—
colorToComplex_comp_eq_match 📖	mathematical	—	Color complexLorentzTensor.Color colorToComplex	—	—
colorToComplex_match_down 📖	mathematical	Color.down	complexLorentzTensor.Color.down	—	—
colorToComplex_match_up 📖	mathematical	Color.up	complexLorentzTensor.Color.up	—	—
complex_repDim_down 📖	mathematical	—	TensorSpecies.repDim complexLorentzTensor.Color complexLorentzTensor complexLorentzTensor.Color.down	—	—
complex_repDim_up 📖	mathematical	—	TensorSpecies.repDim complexLorentzTensor.Color complexLorentzTensor complexLorentzTensor.Color.up	—	—
complexify_prod 📖	mathematical	—	TensorSpecies.Tensor.ComponentIdx Color LorentzGroup lorentzGroupIsGroup realLorentzTensor complexLorentzTensor.Color complexLorentzTensor colorToComplex TensorSpecies.Tensor.ComponentIdx.complexify TensorSpecies.Tensor.ComponentIdx.prod colorToComplex_append	—	colorToComplex_append ComponentIdx.complexify_apply TensorSpecies.Tensor.ComponentIdx.prod_apply_finSumFinEquiv
contrT_toComplex 📖	mathematical	TensorSpecies.τ Color LorentzGroup lorentzGroupIsGroup realLorentzTensor	TensorSpecies.Tensor Color LorentzGroup lorentzGroupIsGroup realLorentzTensor TensorSpecies.Tensor.Pure.dropPairEmb complexLorentzTensor.Color complexLorentzTensor colorToComplex IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F toComplex TensorSpecies.Tensor.contrT	—	tau_colorToComplex TensorSpecies.Tensor.induction_on_basis TensorSpecies.Tensor.basis_apply TensorSpecies.Tensor.contrT_pure toComplex_pure_basisVector toComplex_contrP_basisVector
evalT_toComplex 📖	mathematical	—	TensorSpecies.Tensor Color LorentzGroup lorentzGroupIsGroup realLorentzTensor complexLorentzTensor.Color complexLorentzTensor colorToComplex IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F toComplex TensorSpecies.Tensor.evalT evalTColorToComplex	—	TensorSpecies.Tensor.induction_on_basis TensorSpecies.Tensor.basis_apply TensorSpecies.Tensor.evalT_pure toComplex_pure_basisVector toComplex_evalP_basisVector toComplex_map_smul
permCond_colorToComplex 📖	mathematical	TensorSpecies.Tensor.PermCond Color	TensorSpecies.Tensor.PermCond complexLorentzTensor.Color Color colorToComplex	—	—
permCond_prodTColorToComplex 📖	mathematical	—	TensorSpecies.Tensor.PermCond complexLorentzTensor.Color Color colorToComplex	—	TensorSpecies.Tensor.PermCond.on_id colorToComplex_append
permT_basis_complex 📖	mathematical	TensorSpecies.Tensor.PermCond complexLorentzTensor.Color	TensorSpecies.Tensor complexLorentzTensor.Color complexLorentzTensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.permT TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.basis TensorSpecies.repDim	—	TensorSpecies.Tensor.basis_apply TensorSpecies.Tensor.permT_pure TensorSpecies.Tensor.Pure.permP_basisVector
permT_basis_real 📖	mathematical	TensorSpecies.Tensor.PermCond Color	TensorSpecies.Tensor Color LorentzGroup lorentzGroupIsGroup realLorentzTensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.permT TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.basis TensorSpecies.repDim	—	TensorSpecies.Tensor.basis_apply TensorSpecies.Tensor.permT_pure TensorSpecies.Tensor.Pure.permP_basisVector
permT_toComplex 📖	mathematical	TensorSpecies.Tensor.PermCond Color	TensorSpecies.Tensor Color LorentzGroup lorentzGroupIsGroup realLorentzTensor complexLorentzTensor.Color complexLorentzTensor colorToComplex IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F toComplex TensorSpecies.Tensor.permT permCond_colorToComplex	—	permCond_colorToComplex TensorSpecies.Tensor.induction_on_basis permT_basis_real toComplex_basis permT_basis_complex
prodT_toComplex 📖	mathematical	—	TensorSpecies.Tensor Color LorentzGroup lorentzGroupIsGroup realLorentzTensor complexLorentzTensor.Color complexLorentzTensor colorToComplex IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F toComplex TensorSpecies.Tensor.prodT prodTColorToComplex	—	TensorSpecies.Tensor.induction_on_basis colorToComplex_append TensorSpecies.Tensor.basis_apply TensorSpecies.Tensor.prodT_pure TensorSpecies.Tensor.Pure.prodP_basisVector toComplex_pure_basisVector complexify_prod permCond_prodTColorToComplex TensorSpecies.Tensor.permT_congr TensorSpecies.Tensor.permT_pure TensorSpecies.Tensor.Pure.permP_basisVector toComplex_basis
tau_colorToComplex 📖	mathematical	—	TensorSpecies.τ complexLorentzTensor.Color complexLorentzTensor colorToComplex Color LorentzGroup lorentzGroupIsGroup realLorentzTensor	—	—
toComplex_basis 📖	mathematical	—	TensorSpecies.Tensor Color LorentzGroup lorentzGroupIsGroup realLorentzTensor complexLorentzTensor.Color complexLorentzTensor colorToComplex IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F toComplex TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.basis TensorSpecies.Tensor.ComponentIdx.complexify	—	—
toComplex_contrP_basisVector 📖	mathematical	TensorSpecies.τ Color LorentzGroup lorentzGroupIsGroup realLorentzTensor	TensorSpecies.Tensor Color LorentzGroup lorentzGroupIsGroup realLorentzTensor TensorSpecies.Tensor.Pure.dropPairEmb complexLorentzTensor.Color complexLorentzTensor colorToComplex IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F toComplex TensorSpecies.Tensor.Pure.contrP TensorSpecies.Tensor.Pure.basisVector TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.ComponentIdx.complexify	—	toComplex_map_smul TensorSpecies.Tensor.Pure.dropPair_basisVector TensorSpecies.Tensor.basis_apply toComplex_basis contr_basis tau_colorToComplex complexLorentzTensor.basis_contr TensorSpecies.basis_congr TensorSpecies.castToField_eq_self ComponentIdx.complexify_comp_dropPairEmb
toComplex_eq_sum_basis 📖	mathematical	—	TensorSpecies.Tensor Color LorentzGroup lorentzGroupIsGroup realLorentzTensor complexLorentzTensor.Color complexLorentzTensor colorToComplex IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F toComplex TensorSpecies.Tensor.ComponentIdx TensorSpecies.repDim TensorSpecies.Tensor.basis TensorSpecies.Tensor.ComponentIdx.complexify	—	—
toComplex_eq_zero_iff 📖	mathematical	—	TensorSpecies.Tensor Color LorentzGroup lorentzGroupIsGroup realLorentzTensor complexLorentzTensor.Color complexLorentzTensor colorToComplex IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F toComplex	—	toComplex_eq_sum_basis
toComplex_equivariant 📖	mathematical	—	TensorSpecies.Tensor complexLorentzTensor.Color complexLorentzTensor Color colorToComplex TensorSpecies.Tensorial.smulAction IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensorial.self LorentzGroup lorentzGroupIsGroup realLorentzTensor toComplex Lorentz.SL2C.toLorentzGroup	—	TensorSpecies.Tensor.induction_on_basis toComplex_basis TensorSpecies.Tensor.basis_apply TensorSpecies.Tensor.actionT_pure TensorSpecies.Tensor.basis_repr_pure toComplex_repr TensorSpecies.Tensor.Pure.actionP_eq colorToComplex_comp_eq_match colorToComplex_match_up complexLorentzTensor.repr_ρ_basis_vector_up_of_eq toComplex_equivariant_slot_repr_up colorToComplex_match_down complexLorentzTensor.repr_ρ_basis_vector_down_of_eq toComplex_equivariant_slot_repr_down toComplex_map_smul TensorSpecies.Tensor.actionT_smul TensorSpecies.Tensor.actionT_add
toComplex_equivariant_slot_repr_down 📖	mathematical	Color.down	TensorSpecies.repDim Color LorentzGroup lorentzGroupIsGroup realLorentzTensor TensorSpecies.FD TensorSpecies.basis Lorentz.SL2C.toLorentzGroup TensorSpecies.Tensor.ComponentIdx complexLorentzTensor.Color complexLorentzTensor colorToComplex TensorSpecies.Tensor.ComponentIdx.complexify LorentzGroup.toComplex	—	TensorSpecies.repr_ρ_basis_FDTransport repDim_eq_one_plus_dim Lorentz.coBasis_ρ_apply LorentzGroup.toComplex_inv LorentzGroup.coe_inv
toComplex_equivariant_slot_repr_up 📖	mathematical	Color.up	TensorSpecies.repDim Color LorentzGroup lorentzGroupIsGroup realLorentzTensor TensorSpecies.FD TensorSpecies.basis Lorentz.SL2C.toLorentzGroup TensorSpecies.Tensor.ComponentIdx complexLorentzTensor.Color complexLorentzTensor colorToComplex TensorSpecies.Tensor.ComponentIdx.complexify LorentzGroup.toComplex	—	TensorSpecies.repr_ρ_basis_FDTransport repDim_eq_one_plus_dim Lorentz.contrBasis_ρ_apply
toComplex_evalP_basisVector 📖	mathematical	—	TensorSpecies.Tensor Color LorentzGroup lorentzGroupIsGroup realLorentzTensor complexLorentzTensor.Color complexLorentzTensor colorToComplex IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F toComplex TensorSpecies.Tensor.Pure.evalP TensorSpecies.Tensor.Pure.basisVector TensorSpecies.Tensor.permT evalIdxToComplex TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.ComponentIdx.complexify	—	toComplex_map_smul toComplex_pure_basisVector TensorSpecies.Tensor.permT_congr TensorSpecies.Tensor.permT_id_self
toComplex_injective 📖	mathematical	—	TensorSpecies.Tensor Color LorentzGroup lorentzGroupIsGroup realLorentzTensor complexLorentzTensor.Color complexLorentzTensor colorToComplex IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F toComplex	—	toComplex_eq_zero_iff
toComplex_map_smul 📖	mathematical	—	TensorSpecies.Tensor Color LorentzGroup lorentzGroupIsGroup realLorentzTensor complexLorentzTensor.Color complexLorentzTensor colorToComplex IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F toComplex	—	—
toComplex_pure_basisVector 📖	mathematical	—	TensorSpecies.Tensor Color LorentzGroup lorentzGroupIsGroup realLorentzTensor complexLorentzTensor.Color complexLorentzTensor colorToComplex IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F toComplex TensorSpecies.Tensor.Pure.toTensor TensorSpecies.Tensor.Pure.basisVector TensorSpecies.Tensor.ComponentIdx TensorSpecies.Tensor.ComponentIdx.complexify	—	TensorSpecies.Tensor.basis_apply toComplex_basis
toComplex_repr 📖	mathematical	—	TensorSpecies.Tensor.ComponentIdx complexLorentzTensor.Color complexLorentzTensor Color colorToComplex TensorSpecies.Tensor IndexNotation.OverColor IndexNotation.instGroupoidOverColor TensorSpecies.F TensorSpecies.Tensor.basis LorentzGroup lorentzGroupIsGroup realLorentzTensor toComplex TensorSpecies.Tensor.ComponentIdx.complexify	—	toComplex_eq_sum_basis

realLorentzTensor.ComponentIdx

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
complexify_apply 📖	mathematical	—	TensorSpecies.Tensor.ComponentIdx realLorentzTensor.Color LorentzGroup lorentzGroupIsGroup realLorentzTensor complexLorentzTensor.Color complexLorentzTensor realLorentzTensor.colorToComplex TensorSpecies.Tensor.ComponentIdx.complexify TensorSpecies.repDim	—	—
complexify_comp_dropPairEmb 📖	mathematical	—	TensorSpecies.Tensor.ComponentIdx realLorentzTensor.Color LorentzGroup lorentzGroupIsGroup realLorentzTensor TensorSpecies.Tensor.Pure.dropPairEmb complexLorentzTensor.Color complexLorentzTensor realLorentzTensor.colorToComplex TensorSpecies.Tensor.ComponentIdx.complexify	—	—
complexify_comp_succAbove 📖	mathematical	—	TensorSpecies.Tensor.ComponentIdx realLorentzTensor.Color LorentzGroup lorentzGroupIsGroup realLorentzTensor complexLorentzTensor.Color complexLorentzTensor realLorentzTensor.colorToComplex TensorSpecies.Tensor.ComponentIdx.complexify	—	—
complexify_toFun_apply 📖	mathematical	—	TensorSpecies.Tensor.ComponentIdx realLorentzTensor.Color LorentzGroup lorentzGroupIsGroup realLorentzTensor complexLorentzTensor.Color complexLorentzTensor realLorentzTensor.colorToComplex TensorSpecies.Tensor.ComponentIdx.complexify	—	—

---

← Back to Index