Documentation Verification Report

ToComplex

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

Statistics

Metric	Count
Definitions `complexify`, `colorToComplex`, `evalIdxToComplex`, `evalTColorToComplex`, `prodTColorToComplex`, `toComplex`	6
Theorems `colorToComplex_append`, `complex_repDim_down`, `complex_repDim_up`, `contrT_toComplex`, `evalT_toComplex`, `permCond_colorToComplex`, `permT_toComplex`, `prodT_toComplex`, `tau_colorToComplex`, `toComplex_eq_sum_basis`, `toComplex_eq_zero_iff`, `toComplex_equivariant`, `toComplex_injective`	13
Total	19
⚠️ With sorry `contrT_toComplex`, `evalT_toComplex`, `permT_toComplex`, `prodT_toComplex`, `toComplex_equivariant`	5

TensorSpecies.Tensor.ComponentIdx

Definitions

Name	Category	Theorems
`complexify` 📖	CompOp	1 math math: `realLorentzTensor.toComplex_eq_sum_basis`

realLorentzTensor

Definitions

Name	Category	Theorems
`colorToComplex` 📖	CompOp	11 math math: `prodT_toComplex`, `tau_colorToComplex`, `toComplex_injective`, `contrT_toComplex`, `colorToComplex_append`, `toComplex_eq_sum_basis`, `permT_toComplex`, `evalT_toComplex`, `toComplex_equivariant`, `toComplex_eq_zero_iff`, `permCond_colorToComplex`
`evalIdxToComplex` 📖	CompOp	—
`evalTColorToComplex` 📖	CompOp	1 math math: `evalT_toComplex`
`prodTColorToComplex` 📖	CompOp	1 math math: `prodT_toComplex`
`toComplex` 📖	CompOp	8 math math: `prodT_toComplex`, `toComplex_injective`, `contrT_toComplex`, `toComplex_eq_sum_basis`, `permT_toComplex`, `evalT_toComplex`, `toComplex_equivariant`, `toComplex_eq_zero_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`colorToComplex_append` 📖	mathematical	—	`Color` `complexLorentzTensor.Color` `colorToComplex`	—	—
`complex_repDim_down` 📖	mathematical	—	`TensorSpecies.repDim` `complexLorentzTensor.Color` `complexLorentzTensor` `complexLorentzTensor.Color.down`	—	—
`complex_repDim_up` 📖	mathematical	—	`TensorSpecies.repDim` `complexLorentzTensor.Color` `complexLorentzTensor` `complexLorentzTensor.Color.up`	—	—
`contrT_toComplex` 📖 ⚠️	mathematical	`TensorSpecies.τ` `Color` `LorentzGroup` `lorentzGroupIsGroup` `realLorentzTensor`	`TensorSpecies.Tensor` `TensorSpecies.Tensor.Pure.dropPairEmb` `complexLorentzTensor.Color` `complexLorentzTensor` `colorToComplex` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `toComplex` `TensorSpecies.Tensor.contrT` `tau_colorToComplex`	—	`tau_colorToComplex`
`evalT_toComplex` 📖 ⚠️	mathematical	—	`TensorSpecies.Tensor` `Color` `LorentzGroup` `lorentzGroupIsGroup` `realLorentzTensor` `complexLorentzTensor.Color` `complexLorentzTensor` `colorToComplex` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `toComplex` `TensorSpecies.Tensor.evalT` `evalTColorToComplex`	—	—
`permCond_colorToComplex` 📖	mathematical	`TensorSpecies.Tensor.PermCond` `Color`	`complexLorentzTensor.Color` `colorToComplex`	—	—
`permT_toComplex` 📖 ⚠️	mathematical	`TensorSpecies.Tensor.PermCond` `Color`	`TensorSpecies.Tensor` `LorentzGroup` `lorentzGroupIsGroup` `realLorentzTensor` `complexLorentzTensor.Color` `complexLorentzTensor` `colorToComplex` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `toComplex` `TensorSpecies.Tensor.permT` `permCond_colorToComplex`	—	`permCond_colorToComplex`
`prodT_toComplex` 📖 ⚠️	mathematical	—	`TensorSpecies.Tensor` `Color` `LorentzGroup` `lorentzGroupIsGroup` `realLorentzTensor` `complexLorentzTensor.Color` `complexLorentzTensor` `colorToComplex` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `toComplex` `TensorSpecies.Tensor.prodT` `prodTColorToComplex`	—	—
`tau_colorToComplex` 📖	mathematical	—	`TensorSpecies.τ` `complexLorentzTensor.Color` `complexLorentzTensor` `colorToComplex` `Color` `LorentzGroup` `lorentzGroupIsGroup` `realLorentzTensor`	—	—
`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`	—	—
`toComplex_injective` 📖	mathematical	—	`TensorSpecies.Tensor` `Color` `LorentzGroup` `lorentzGroupIsGroup` `realLorentzTensor` `complexLorentzTensor.Color` `complexLorentzTensor` `colorToComplex` `IndexNotation.OverColor` `IndexNotation.instGroupoidOverColor` `TensorSpecies.F` `toComplex`	—	`toComplex_eq_zero_iff`

---

← Back to Index