Documentation Verification Report

Pre

📁 Source: PhysLean/Relativity/Tensors/RealTensor/Matrix/Pre.lean

Statistics

Metric	Count
Definitions `coCoToMatrixRe`, `coContrToMatrixRe`, `contrCoToMatrixRe`, `contrContrToMatrixRe`	4
Theorems `coCoToMatrixRe_symm_expand_tmul`, `coCoToMatrixRe_ρ`, `coCoToMatrixRe_ρ_symm`, `coContrToMatrixRe_symm_expand_tmul`, `coContrToMatrixRe_ρ`, `coContrToMatrixRe_ρ_symm`, `contrCoToMatrixRe_symm_expand_tmul`, `contrCoToMatrixRe_ρ`, `contrCoToMatrixRe_ρ_symm`, `contrContrToMatrixRe_symm_expand_tmul`, `contrContrToMatrixRe_ρ`, `contrContrToMatrixRe_ρ_symm`	12
Total	16

Lorentz

Definitions

Name	Category	Theorems
`coCoToMatrixRe` 📖	CompOp	3 math math: `coCoToMatrixRe_symm_expand_tmul`, `coCoToMatrixRe_ρ`, `coCoToMatrixRe_ρ_symm`
`coContrToMatrixRe` 📖	CompOp	3 math math: `coContrToMatrixRe_symm_expand_tmul`, `coContrToMatrixRe_ρ_symm`, `coContrToMatrixRe_ρ`
`contrCoToMatrixRe` 📖	CompOp	3 math math: `contrCoToMatrixRe_ρ`, `contrCoToMatrixRe_symm_expand_tmul`, `contrCoToMatrixRe_ρ_symm`
`contrContrToMatrixRe` 📖	CompOp	3 math math: `contrContrToMatrixRe_symm_expand_tmul`, `contrContrToMatrixRe_ρ_symm`, `contrContrToMatrixRe_ρ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coCoToMatrixRe_symm_expand_tmul` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Co` `coCoToMatrixRe` `coBasis`	—	—
`coCoToMatrixRe_ρ` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Co` `coCoToMatrixRe`	—	`coCoToMatrixRe.eq_1` `coBasis_ρ_apply`
`coCoToMatrixRe_ρ_symm` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Co` `coCoToMatrixRe`	—	`coCoToMatrixRe_ρ`
`coContrToMatrixRe_symm_expand_tmul` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Co` `Contr` `coContrToMatrixRe` `coBasis` `contrBasis`	—	—
`coContrToMatrixRe_ρ` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Co` `Contr` `coContrToMatrixRe`	—	`coContrToMatrixRe.eq_1` `coBasis_ρ_apply` `contrBasis_ρ_apply`
`coContrToMatrixRe_ρ_symm` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Co` `Contr` `coContrToMatrixRe`	—	`coContrToMatrixRe_ρ`
`contrCoToMatrixRe_symm_expand_tmul` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Contr` `Co` `contrCoToMatrixRe` `contrBasis` `coBasis`	—	—
`contrCoToMatrixRe_ρ` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Contr` `Co` `contrCoToMatrixRe`	—	`contrCoToMatrixRe.eq_1` `contrBasis_ρ_apply` `coBasis_ρ_apply`
`contrCoToMatrixRe_ρ_symm` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Contr` `Co` `contrCoToMatrixRe`	—	`contrCoToMatrixRe_ρ`
`contrContrToMatrixRe_symm_expand_tmul` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Contr` `contrContrToMatrixRe` `contrBasis`	—	—
`contrContrToMatrixRe_ρ` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Contr` `contrContrToMatrixRe`	—	`contrContrToMatrixRe.eq_1` `contrBasis_ρ_apply`
`contrContrToMatrixRe_ρ_symm` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `Contr` `contrContrToMatrixRe`	—	`contrContrToMatrixRe_ρ`

---

← Back to Index