Documentation Verification Report

Modules

📁 Source: PhysLean/Relativity/Tensors/ComplexTensor/Vector/Pre/Modules.lean

Statistics

Metric	Count
Definitions `ContrℂModule`, `SL2CRep`, `instAddCommGroup`, `instAddCommMonoid`, `instModuleComplex`, `lorentzGroupRep`, `toFin13ℂ`, `toFin13ℂEquiv`, `toFin13ℂFun`, `val`, `CoℂModule`, `SL2CRep`, `instAddCommGroup`, `instAddCommMonoid`, `instModuleComplex`, `lorentzGroupRep`, `toFin13ℂ`, `toFin13ℂEquiv`, `toFin13ℂFun`, `val`	20
Theorems `ext`, `ext_iff`, `toFin13ℂEquiv_apply`, `toFin13ℂEquiv_symm_apply_val`, `val_add`, `val_smul`, `toFin13ℂEquiv_apply`, `toFin13ℂEquiv_symm_apply_val`	8
Total	28

Lorentz

Definitions

Name	Category	Theorems
`ContrℂModule` 📖	CompData	4 math math: `ContrℂModule.val_smul`, `ContrℂModule.toFin13ℂEquiv_apply`, `ContrℂModule.toFin13ℂEquiv_symm_apply_val`, `ContrℂModule.val_add`
`CoℂModule` 📖	CompData	2 math math: `CoℂModule.toFin13ℂEquiv_symm_apply_val`, `CoℂModule.toFin13ℂEquiv_apply`

Lorentz.ContrℂModule

Definitions

Name	Category	Theorems
`SL2CRep` 📖	CompOp	—
`instAddCommGroup` 📖	CompOp	1 math math: `val_smul`
`instAddCommMonoid` 📖	CompOp	4 math math: `val_smul`, `toFin13ℂEquiv_apply`, `toFin13ℂEquiv_symm_apply_val`, `val_add`
`instModuleComplex` 📖	CompOp	3 math math: `val_smul`, `toFin13ℂEquiv_apply`, `toFin13ℂEquiv_symm_apply_val`
`lorentzGroupRep` 📖	CompOp	—
`toFin13ℂ` 📖	CompOp	3 math math: `Lorentz.complexContrBasis_toFin13ℂ`, `Lorentz.contrCoContraction_hom_tmul`, `Lorentz.coContrContraction_hom_tmul`
`toFin13ℂEquiv` 📖	CompOp	2 math math: `toFin13ℂEquiv_apply`, `toFin13ℂEquiv_symm_apply_val`
`toFin13ℂFun` 📖	CompOp	1 math math: `toFin13ℂEquiv_apply`
`val` 📖	CompOp	6 math math: `val_smul`, `Lorentz.inclCongrRealLorentz_val`, `ext_iff`, `Lorentz.complexContrBasis_ρ_val`, `toFin13ℂEquiv_symm_apply_val`, `val_add`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`val`	—	—	—
`ext_iff` 📖	mathematical	—	`val`	—	`ext`
`toFin13ℂEquiv_apply` 📖	mathematical	—	`Lorentz.ContrℂModule` `instAddCommMonoid` `instModuleComplex` `toFin13ℂEquiv` `toFin13ℂFun`	—	—
`toFin13ℂEquiv_symm_apply_val` 📖	mathematical	—	`val` `Lorentz.ContrℂModule` `instAddCommMonoid` `instModuleComplex` `toFin13ℂEquiv`	—	—
`val_add` 📖	mathematical	—	`val` `Lorentz.ContrℂModule` `instAddCommMonoid`	—	—
`val_smul` 📖	mathematical	—	`val` `Lorentz.ContrℂModule` `instAddCommGroup` `instAddCommMonoid` `instModuleComplex`	—	—

Lorentz.CoℂModule

Definitions

Name	Category	Theorems
`SL2CRep` 📖	CompOp	—
`instAddCommGroup` 📖	CompOp	—
`instAddCommMonoid` 📖	CompOp	2 math math: `toFin13ℂEquiv_symm_apply_val`, `toFin13ℂEquiv_apply`
`instModuleComplex` 📖	CompOp	2 math math: `toFin13ℂEquiv_symm_apply_val`, `toFin13ℂEquiv_apply`
`lorentzGroupRep` 📖	CompOp	—
`toFin13ℂ` 📖	CompOp	3 math math: `Lorentz.complexCoBasis_toFin13ℂ`, `Lorentz.contrCoContraction_hom_tmul`, `Lorentz.coContrContraction_hom_tmul`
`toFin13ℂEquiv` 📖	CompOp	2 math math: `toFin13ℂEquiv_symm_apply_val`, `toFin13ℂEquiv_apply`
`toFin13ℂFun` 📖	CompOp	1 math math: `toFin13ℂEquiv_apply`
`val` 📖	CompOp	1 math math: `toFin13ℂEquiv_symm_apply_val`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toFin13ℂEquiv_apply` 📖	mathematical	—	`Lorentz.CoℂModule` `instAddCommMonoid` `instModuleComplex` `toFin13ℂEquiv` `toFin13ℂFun`	—	—
`toFin13ℂEquiv_symm_apply_val` 📖	mathematical	—	`val` `Lorentz.CoℂModule` `instAddCommMonoid` `instModuleComplex` `toFin13ℂEquiv`	—	—

---

← Back to Index